English
Under T1Space X, the support is discrete inside U if the ambient space supports discrete topology on the support.
Русский
При T1-пространстве X опора дискретна внутри U при условии дискретной топологии на опоре.
LaTeX
$$$\\text{DiscreteTopology}(D^{\\text{support}})$.$$
Lean4
/-- If `X` is T1 and if `U` is closed, then the support of support of a function with locally finite
support within `U` is also closed.
-/
theorem closedSupport [T1Space X] [Zero Y] (D : locallyFinsuppWithin U Y) (hU : IsClosed U) : IsClosed D.support :=
by
convert
isClosed_sdiff_of_codiscreteWithin
((supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2 D.supportLocallyFiniteWithinDomain) hU
ext x
constructor <;> intro hx
· simp_all [D.supportWithinDomain hx]
· simp_all
