iSup_bool_eq — Mathlib

English

In any complete lattice, the supremum over a two-point Bool index is the maximum of the two values f(true) and f(false).

Русский

В полной решетке верхняя граница по индексу Bool равна максимуму значений f(true) и f(false).

LaTeX

$$$$ \\sup_{b \\in \\{\\text{true},\\text{false}\\}} f(b) = \\max\\left\\{ f(\\text{true}), f(\\text{false}) \\right\\} $$$$

Lean4

theorem iSup_bool_eq {f : Bool → α} : ⨆ b : Bool, f b = f true ⊔ f false := by
  rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

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