iSup_option — Mathlib

English

For a function f: Option β → α, the supremum over all options equals the maximum of the value at none and the supremum over all some values: ⨆ o, f o = f none ⊔ ⨆ b, f (Some b).

Русский

Для функции f: Option β → α верхняя граница по всем Option равна максимуму значения в none и верхней границы по всем some b: ⨆ o, f o = f none ⊔ ⨆ b, f (Some b).

LaTeX

$$$\\displaystyle \\big\\vee_{o} f(o) = f(\\text{none}) \\;\\sqcup\\; \\big\\vee_{b} f(\\text{Some } b)$$$

Lean4

theorem iSup_option (f : Option β → α) : ⨆ o, f o = f none ⊔ ⨆ b, f (Option.some b) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, sup_le_iff, Option.forall]

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