iInf_univ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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