Commit 2024-09-19 18:37 7d7d3bfa

View on Github →

feat(Topology/AlexandrovDiscrete): generalize some lemmas (#16932)

add mem_exterior_iff_specializes;
prove IsCompact.exterior_iff;
drop [AlexandrovDiscrete _] assumption in some lemmas.

Estimated changes

Modified Mathlib/Topology/AlexandrovDiscrete.lean

added theorem IsCompact.exterior_iff

deleted theorem IsOpen.exterior_subset_iff

modified theorem Set.Finite.isCompact_exterior

added theorem exterior_eq_exterior_iff_nhdsSet

modified theorem exterior_exterior

added theorem exterior_iUnion

added theorem exterior_sUnion

modified theorem exterior_subset_exterior

added theorem exterior_subset_exterior_iff_nhdsSet

modified theorem exterior_union

added theorem mem_exterior_iff_specializes

added theorem mem_exterior_singleton