exists_forall_eventually_atTop_eventually_eq'

English

Duplicate of the nhdsWithin iUnion result for locally finite families.

Русский

Дубликат результата nhdsWithin для локально конечной семейства.

LaTeX

$$LocallyFinite f → ∀ a, 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a$$

Lean4

/-- Let `f : ℕ → Π a, β a` be a sequence of (dependent) functions on a topological space. Suppose
that the family of sets `s n = {x | f (n + 1) x ≠ f n x}` is locally finite. Then there exists a
function `F : Π a, β a` such that for any `x`, for sufficiently large values of `n`, we have
`f n y = F y` in a neighbourhood of `x`. -/
theorem exists_forall_eventually_atTop_eventually_eq' {π : X → Sort*} {f : ℕ → ∀ x : X, π x}
    (hf : LocallyFinite fun n => {x | f (n + 1) x ≠ f n x}) :
    ∃ F : ∀ x : X, π x, ∀ x, ∀ᶠ n : ℕ in atTop, ∀ᶠ y : X in 𝓝 x, f n y = F y :=
  hf.exists_forall_eventually_eq_prod.imp fun _F hF x => (hF x).curry

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