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 }