Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-18 12:22 be9a5dec

View on Github →

feat(topology/separation): add t1_space_tfae (#11534) Also add some lemmas about filter.disjoint.

Estimated changes

Modified src/order/filter/bases.lean

added theorem filter.disjoint_principal_left

added theorem filter.disjoint_principal_principal

added theorem filter.disjoint_principal_right

added theorem filter.disjoint_pure_pure

added theorem filter.has_basis.disjoint_basis_iff

deleted theorem filter.inf_eq_bot_iff

deleted theorem filter.le_iff_forall_disjoint_principal_compl

deleted theorem filter.mem_iff_disjoint_principal_compl

Modified src/order/filter/basic.lean

added theorem filter.inf_eq_bot_iff

Modified src/topology/algebra/ordered/basic.lean

Modified src/topology/separation.lean

added theorem disjoint_nhds_pure

added theorem disjoint_pure_nhds

deleted theorem finite.is_closed

deleted theorem t1_iff_exists_open

deleted theorem t1_space_antimono

added theorem t1_space_antitone

added theorem t1_space_iff_disjoint_nhds_pure

added theorem t1_space_iff_disjoint_pure_nhds

added theorem t1_space_iff_exists_open

added theorem t1_space_tfae