ofBoolAlg — Mathlib

English

Let α be a type equipped with a Boolean ring structure. There is a canonical equivalence between the Boolean algebra AsBoolAlg α and the underlying set α, given by the identity on α.

Русский

Пусть α — тип, снабжённый структурой булевого кольца. Существует каноническое эквивалентное отображение между булевой алгеброй AsBoolAlg α и базовым множеством α, заданное идентичностью на α.

LaTeX

$$$\mathrm{ofBoolAlg} : \mathrm{AsBoolAlg}(\alpha) \cong \alpha$$$

Lean4

/-- The "identity" equivalence between `α` and `AsBoolAlg α`. -/
def ofBoolAlg : AsBoolAlg α ≃ α :=
  Equiv.refl _

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