orderIsoBool — Mathlib

English

There exists an order isomorphism from the simple order to Bool.

Русский

Существует порядок-изоморфизм между простым порядком и Bool.

LaTeX

$$$\text{orderIsoBool} : α \simeq_{\mathrm{ord}} Bool$$$

Lean4

/-- Every simple lattice over a partial order is order-isomorphic to `Bool`. -/
def orderIsoBool : α ≃o Bool :=
  { equivBool with
    map_rel_iff' :=
      @fun a b => by
        rcases eq_bot_or_eq_top a with (rfl | rfl)
        · simp
        · rcases eq_bot_or_eq_top b with (rfl | rfl)
          · simp [bot_ne_top.symm, Bool.false_lt_true]
          · simp }

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