supportDiscreteWithin_iff_locallyFiniteWithin

English

For any function D that has locally finite support within U, its support is contained in U.

Русский

Для любой функции D с локально конечной опорой внутри U её опора содержится в U.

LaTeX

$$$D\\text{.support} \\subseteq U$$$

Lean4

/-- For T1 spaces, the condition `supportLocallyFiniteWithinDomain'` is equivalent to saying that the
support is codiscrete within `U`.
-/
theorem supportDiscreteWithin_iff_locallyFiniteWithin [T1Space X] [Zero Y] {f : X → Y} (h : f.support ⊆ U) :
    f =ᶠ[codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support) :=
  by
  have : f.support = (U \ {x | f x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, mem_diff, mem_setOf_eq, iff_and_self]
    exact (h ·)
  rw [EventuallyEq, Filter.Eventually, codiscreteWithin_iff_locallyFiniteComplementWithin, this]

Похожие утверждения