iSup_option_elim — Mathlib

English

A convenient form of iSup_option: for any a ∈ α and f: β → α, the supremum over o : Option β of o.elim a f equals a ⊔ sup_{b} f b.

Русский

Удобная форма iSup_option: для любых a и f: β → α, верхняя граница по o : Option β от o.elim a f равна a ⊔ sup_{b} f(b).

LaTeX

$$$\\displaystyle \\big\\vee_{o:\\mathrm{Option}\\,\\beta} (o.elim\\ a\\ f) = a \\;\\sqcup\\; \\big\\vee_{b} f(b)$$$

Lean4

/-- A version of `iSup_option` useful for rewriting right-to-left. -/
theorem iSup_option_elim (a : α) (f : β → α) : ⨆ o : Option β, o.elim a f = a ⊔ ⨆ b, f b := by simp [iSup_option]

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