iInf_bool_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_bool_eq {f : Bool → α} : ⨅ b : Bool, f b = f true ⊓ f false :=
  @iSup_bool_eq αᵒᵈ _ _

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