Commit 2026-09-01 15:53 e8b1229d

View on Github →

feat: IsLocallyClosedAt predicate (#42196)

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.inter_eq_inter_mono_left

added theorem Set.inter_eq_inter_mono_right

added theorem Set.union_eq_union_mono_left

added theorem Set.union_eq_union_mono_right

Modified Mathlib/Order/Lattice.lean

added theorem sup_eq_sup_mono_left

added theorem sup_eq_sup_mono_right

Modified Mathlib/Topology/Defs/Filter.lean

added def IsLocallyClosedAt

Modified Mathlib/Topology/LocallyClosed.lean

added theorem IsLocallyClosed.isLocallyClosedAt

deleted theorem IsLocallyClosed.isOpen_preimage_val_closure

added theorem IsLocallyClosedAt.inter

added theorem IsLocallyClosedAt.of_mem_nhds

added theorem IsLocallyClosedAt.of_notMem_closure

added theorem IsLocallyClosedAt.preimage

added theorem IsLocallyClosedAt.union

added theorem interior_coborder

added theorem isLocallyClosedAt_iff_closure_eventuallyLE

added theorem isLocallyClosedAt_iff_coborder_mem_nhds

added theorem isLocallyClosedAt_iff_eventuallyEq_closure

added theorem isLocallyClosedAt_iff_exists_eq_inter_closure

added theorem isLocallyClosedAt_iff_exists_eq_inter_closure_of_hasBasis

added theorem isLocallyClosedAt_iff_exists_inter_closure_subset

added theorem isLocallyClosedAt_iff_exists_inter_closure_subset_of_hasBasis

added theorem isLocallyClosedAt_iff_exists_isClosed_eventuallyEq

added theorem isLocallyClosedAt_iff_exists_isClosed_inter_eq_of_hasBasis

added theorem isLocallyClosedAt_iff_exists_isClosed_preimage_val

added theorem isLocallyClosedAt_iff_exists_isClosed_preimage_val_of_hasBasis

added theorem isLocallyClosedAt_tfae

added theorem isLocallyClosed_iff_isLocallyClosedAt

added theorem isLocallyClosed_iff_isOpen_preimage_val_closure

added theorem mem_coborder_iff_imp