iSup_univ — Mathlib

English

For any f: β → α, the supremum over the universe equals the supremum over all elements: ⨆ x ∈ univ, f x = ⨆ x, f x.

Русский

Для любого f: β → α супремум по всему универсу равен супремуму по всем элементам: ⨆ x ∈ univ, f x = ⨆ x, f x.

LaTeX

$$$$ \\sup_{x \\in \\mathrm{univ}} f(x) = \\sup_{x} f(x) $$$$

Lean4

theorem iSup_univ {f : β → α} : ⨆ x ∈ (univ : Set β), f x = ⨆ x, f x := by simp

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