Commit 2022-07-26 11:31 a095eaeb

feat(order/filter/*): filter.pi is countably generated (#15632)

• rename filter.has_basis_infi to filter.has_basis_infi', add new filter.has_basis_infi;
• move prod.is_countably_generated, golf, add coprod.is_countably_generated;
• is_countably_generated_seq is no longer an instance, infi.is_countably_generated is better;
• add infi.is_countably_generated and pi.is_countably_generated;
• prove prod.fist_countable_topology (from the sphere eversion project) and pi.first_countable_topology;
• generalize pi.second_countable_topology from encodable to countable so that it automatically applies to finite types.