equivBool — Mathlib

English

Every simple lattice is order-isomorphic to a two-element Boolean algebra.

Русский

Каждый простой решётчатый порядок изоморфен двум элементам булевой алгебры Bool.

LaTeX

$$$\text{IsSimpleOrder.equivBool}(\alpha) : \alpha \cong Bool$$$

Lean4

/-- Every simple lattice is isomorphic to `Bool`, regardless of order. -/
@[simps]
def equivBool {α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] : α ≃ Bool
    where
  toFun x := x = ⊤
  invFun x := x.casesOn ⊥ ⊤
  left_inv x := by rcases eq_bot_or_eq_top x with (rfl | rfl) <;> simp [bot_ne_top]
  right_inv x := by cases x <;> simp [bot_ne_top]

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