Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 10:03 ea9dae21

View on Github →

refactor(topology/*): Use disjoint (#14950) Replace uses of s ∩ t = ∅ by disjoint s t in the topology library. This shortens proofs.

Estimated changes

Modified src/data/set/basic.lean

deleted theorem set.subset_compl_iff_disjoint

Modified src/field_theory/krull_topology.lean

Modified src/group_theory/group_action/basic.lean

added theorem mul_action.disjoint_image_image_iff

Modified src/measure_theory/constructions/polish.lean

Modified src/measure_theory/function/continuous_map_dense.lean

Modified src/measure_theory/measure/haar.lean

Modified src/topology/alexandroff.lean

Modified src/topology/algebra/const_mul_action.lean

Modified src/topology/algebra/continuous_monoid_hom.lean

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

Modified src/topology/basic.lean

added theorem disjoint.frontier_left

added theorem disjoint.frontier_right

deleted theorem is_open.inter_frontier_eq_empty_of_disjoint

modified def is_open

modified theorem is_open_univ

Modified src/topology/compact_open.lean

added theorem continuous_map.gen_empty_right

Modified src/topology/connected.lean

Modified src/topology/local_homeomorph.lean

Modified src/topology/metric_space/emetric_space.lean

modified theorem emetric.ball_disjoint

Modified src/topology/order/priestley.lean

Modified src/topology/paracompact.lean

Modified src/topology/separation.lean

modified theorem t2_separation_compact_nhds

modified theorem t2_space_iff_nhds

Modified src/topology/subset_properties.lean

Modified src/topology/uniform_space/compact_separated.lean

Modified src/topology/uniform_space/separation.lean