Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-27 15:35 396487f9

View on Github →

feat(topology/separation): Adds t2_space instances for disjoint unions (sums and sigma types). (#5113)

Estimated changes

Modified src/data/set/basic.lean

added theorem set.preimage_inl_range_inr

added theorem set.preimage_inr_range_inl

added theorem set.range_inl_inter_range_inr

modified theorem set.range_inl_union_range_inr

added theorem set.range_inr_inter_range_inl

added theorem set.range_inr_union_range_inl

Modified src/topology/constructions.lean

added theorem is_open_range_inl

added theorem is_open_range_inr

Modified src/topology/separation.lean

added theorem separated_by_continuous

added theorem separated_by_open_embedding