eventually_forall_le — Mathlib

English

If TendstoUniformlyOn f g p K and g ≤ u on K, then for all x in K, f i x ≤ v for all i eventually, with u ≤ v.

Русский

Если f сходится равномерно к g на K и g ≤ u на K, то для всех x ∈ K и почти всех i выполняется f i x ≤ v, где u < v.

LaTeX

$$$\\text{TendstoUniformlyOn}(f,g,p,K) \\land (\\forall x\\in K\\, g(x) \\le u) \\Rightarrow \\forall i\\text{ eventually}, \\forall x\\in K, f(i,x) \\le v$$$

Lean4

theorem eventually_forall_le {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
  filter_upwards [hf.eventually_forall_lt huv hg] with i hi x hx using (hi x hx).le

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