Commit 2024-09-24 06:31 50ab2964

View on Github →

chore(AlexandrovDiscrete): move exterior to new files (#16957) I'm going to use exterior in files that don't need to know about AlexandrovDiscrete.

Estimated changes

deleted theorem IsCompact.exterior_iff
deleted theorem IsOpen.exterior_eq
deleted theorem IsOpen.exterior_subset
deleted def exterior
deleted theorem exterior_def
deleted theorem exterior_empty
deleted theorem exterior_eq_empty
deleted theorem exterior_exterior
deleted theorem exterior_iUnion
deleted theorem exterior_minimal
deleted theorem exterior_mono
deleted theorem exterior_sUnion
deleted theorem exterior_subset_exterior
deleted theorem exterior_union
deleted theorem exterior_univ
deleted theorem mem_exterior
deleted theorem mem_exterior_singleton
deleted theorem nhdsSet_exterior
deleted theorem subset_exterior
deleted theorem subset_exterior_iff
added theorem IsCompact.exterior_iff
added def exterior
added theorem IsOpen.exterior_eq
added theorem IsOpen.exterior_subset
added theorem exterior_def
added theorem exterior_empty
added theorem exterior_eq_empty
added theorem exterior_exterior
added theorem exterior_iUnion
added theorem exterior_minimal
added theorem exterior_mono
added theorem exterior_sUnion
added theorem exterior_union
added theorem exterior_univ
added theorem mem_exterior
added theorem mem_exterior_singleton
added theorem nhdsSet_exterior
added theorem subset_exterior
added theorem subset_exterior_iff