iSup_option_toFinset — Mathlib

English

For an Option α o and f: α → β, the supremum over o.toFinset equals the supremum over o: ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x.

Русский

Для опции o и функции f: α → β верно: ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x.

LaTeX

$$$$\\displaystyle \\sup_{x \\in o^{\\mathrm{toFinset}}} f(x) = \\sup_{x \\in o} f(x). $$$$

Lean4

theorem iSup_option_toFinset (o : Option α) (f : α → β) : ⨆ x ∈ o.toFinset, f x = ⨆ x ∈ o, f x := by simp

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