iSup_le_le — Mathlib

English

For f: ℕ→α→ℝ≥0∞ and natural numbers n,k with k≤n, one has f_k ≤ a↦⨆_{ℓ≤n} f_ℓ(a).

Русский

Для f: ℕ→α→ℝ≥0∞ и натуральных n,k с k≤n выполняется f_k ≤ a↦⨆_{ℓ≤n} f_ℓ(a).

LaTeX

$$$$ f_k \\leqslant \\lambda a. \\big\\lbrace \\sup_{\\ell \\le n} f_\\ell(a) \\rbrace, \\text{ если } k \\le n. $$$$

Lean4

theorem iSup_le_le {α : Type*} (f : ℕ → α → ℝ≥0∞) (n k : ℕ) (hk : k ≤ n) : f k ≤ fun x ↦ ⨆ (k) (_ : k ≤ n), f k x :=
  fun x ↦ le_iSup₂ (f := fun k (_ : k ≤ n) ↦ f k x) k hk

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