Commit 2023-09-14 10:14 4bc2392b

View on Github →

feat: Exterior of a set (#6982) In an Alexandrov-discrete space, every set has a smallest neighborhood. We call this neighborhood the exterior of the set. It is completely analogous to the interior, except that all inclusions are reversed.

Estimated changes

modified def Filter.ker
modified theorem Filter.ker_bot
added theorem Filter.ker_def
modified theorem Filter.mem_ker
modified theorem Filter.subset_ker
added theorem AlexandrovDiscrete.sup
added theorem IsOpen.exterior_eq
added theorem IsOpen.exterior_subset
added theorem closure_iUnion
added theorem closure_sUnion
added def exterior
added theorem exterior_def
added theorem exterior_empty
added theorem exterior_eq_empty
added theorem exterior_eq_iff_isOpen
added theorem exterior_exterior
added theorem exterior_mem_nhdsSet
added theorem exterior_minimal
added theorem exterior_mono
added theorem exterior_subset_iff
added theorem exterior_union
added theorem exterior_univ
added theorem gc_exterior_interior
added theorem interior_iInter
added theorem interior_sInter
added theorem isClopen_iInter
added theorem isClopen_iInter₂
added theorem isClopen_iUnion₂
added theorem isClopen_sInter
added theorem isClosed_iUnion₂
added theorem isOpen_exterior
added theorem isOpen_iInter₂
added theorem mem_exterior
added theorem nhdsSet_exterior
added theorem principal_exterior
added theorem subset_exterior
added theorem subset_exterior_iff
added theorem interior_subset_iff
added theorem nhdsSet_le
added theorem ker_nhds
deleted theorem sInter_sets_nhds
modified def separationRel