exists_lb_support — Mathlib

English

The support of the coefficient function for a Cauchy filter is bounded below.

Русский

Опора функции коэффициентов для фильтра Cauchy ограничена снизу.

LaTeX

$$$\operatorname{support}(\mathrm{coeff}(h_{\mathcal F}))$ is bounded below$$

Lean4

theorem exists_lb_support {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) : ∃ N, ∀ n, n < N → coeff hℱ n = 0 :=
  by
  let _ : UniformSpace K := ⊥
  obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ
  refine
    ⟨N, fun n hn ↦
      Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
        ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩
  simp only [pure_zero, nonpos_iff]
  apply
    Filter.mem_of_superset hN
      (fun _ ha ↦ ha _ hn)
        /- The support of `Cauchy.coeff` is bounded below -/

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