English
In a T1 space, the support of a function with locally finite support within U is a discrete subset of U.
Русский
В T1-пространстве опора функции с локально конечной поддержкой внутри U является дискретным подмножеством U.
LaTeX
$$$\\text{DiscreteTopology}(D.select\\operatorname{support})$$$
Lean4
/-- On a T1 space, the support of a functions with locally finite support within `U` is discrete.
-/
theorem discreteSupport [Zero Y] [T1Space X] (D : locallyFinsuppWithin U Y) : DiscreteTopology D.support :=
by
have : D.support = {x | D x = 0}ᶜ ∩ U := by
ext x
constructor
· exact fun hx ↦ ⟨by tauto, D.supportWithinDomain hx⟩
· intro hx
rw [mem_inter_iff, mem_compl_iff, mem_setOf_eq] at hx
tauto
rw [this]
apply discreteTopology_of_codiscreteWithin
apply (supportDiscreteWithin_iff_locallyFiniteWithin D.supportWithinDomain).2
exact D.supportLocallyFiniteWithinDomain
