eventually_forall_lt — Mathlib

English

If a family f converges uniformly on K to g, and g is bounded above by u, then for any v > u, f is eventually bounded by v on K.

Русский

Если семейство функций сходится равномерно на K к g, и g ограничено сверху на u, то для любого v > u последовательность почти всегда ограничена сверху на v на K.

LaTeX

$$$(\\forall u

Lean4

/-- If a sequence of functions converges uniformly on a set to a function `g` which is bounded above
by a value `u`, then the sequence is strictly bounded by any `v` such that `u < v`. -/
theorem eventually_forall_lt {u v : β} (huv : u < v) (hf : TendstoUniformlyOn f g p K) (hg : ∀ x ∈ K, g x ≤ u) :
    ∀ᶠ i in p, ∀ x ∈ K, f i x < v :=
  by
  simp only [tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero, tendsto_iff_eventually,
    eventually_comap, Prod.forall] at *
  conv at hf => enter [2]; rw [eventually_iff_exists_mem]
  have hf2 :=
    hf (fun x ↦ -x.1 + x.2 < -u + v)
      ⟨_, (isOpen_gt' (-u + v)).mem_nhds (by simp [huv]), fun y hy a b hab ↦ (hab.symm ▸ hy :)⟩
  filter_upwards [eventually_prod_principal_iff.mp hf2] with i hi x hx
  simpa using add_lt_add_of_le_of_lt (hg x hx) (hi x hx)

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