toBoolAlg_ofBoolAlg — Mathlib

English

For every a in AsBoolAlg α, applying ofBoolAlg followed by toBoolAlg recovers a; i.e., toBoolAlg(ofBoolAlg(a)) = a.

Русский

Для любого a из AsBoolAlg α применение ofBoolAlg затем toBoolAlg возвращает a; то есть toBoolAlg(ofBoolAlg(a)) = a.

LaTeX

$$$\mathrm{toBoolAlg}(\mathrm{ofBoolAlg}(a)) = a \quad (a : \mathrm{AsBoolAlg}(\alpha))$$$

Lean4

@[simp]
theorem toBoolAlg_ofBoolAlg (a : AsBoolAlg α) : toBoolAlg (ofBoolAlg a) = a :=
  rfl

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