eq_zero_codiscreteWithin — Mathlib

English

In a T1 space, the support of a locally finite function inside U is codiscrete within U.

Русский

В пространстве T1 опора локально конечной функции внутри U является кодискретной в пределах U.

LaTeX

$$$D =^\\text{codiscreteWithin } U \\;0$$$

Lean4

/-- On a T1 space, the support of a function with locally finite support within `U` is discrete within
`U`.
-/
theorem eq_zero_codiscreteWithin [Zero Y] [T1Space X] (D : locallyFinsuppWithin U Y) :
    D =ᶠ[Filter.codiscreteWithin U] 0 :=
  by
  apply codiscreteWithin_iff_locallyFiniteComplementWithin.2
  have : D.support = (U \ {x | D x = (0 : X → Y) x}) := by
    ext x
    simp only [mem_support, ne_eq, Pi.zero_apply, Set.mem_diff, Set.mem_setOf_eq, iff_and_self]
    exact (support_subset_iff.1 D.supportWithinDomain) x
  rw [← this]
  exact D.supportLocallyFiniteWithinDomain

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