iSup_comp_le — Mathlib

English

For any function f: ι' → α and function g: ι → ι', the supremum over x of f(g(x)) is bounded above by the supremum over y of f(y): ⨆ x, f(g x) ≤ ⨆ y, f y.

Русский

Пусть f: ι' → α и g: ι → ι'. Тогда верхняя грань по x от f(g(x)) не превосходит верхнюю грань по y от f(y).

LaTeX

$$$\\\\big\\\\supsymbol x f(g(x)) \\\\le \\\\big\\\\supsymbol y f(y)$$$

Lean4

theorem iSup_comp_le {ι' : Sort*} (f : ι' → α) (g : ι → ι') : ⨆ x, f (g x) ≤ ⨆ y, f y :=
  iSup_mono' fun _ => ⟨_, le_rfl⟩

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