English
There is an order isomorphism Fin(2) ≃o {a,b} for any a<b, sending 0 to a and 1 to b.
Русский
Существует порядок-изоморфизм Fin(2) ≃o {a,b} при a<b, который отправляет 0 в a и 1 в b.
LaTeX
$$$\mathrm{Fin}(2) \cong_o ({a,b}\;\text{Finset})$ with $0\mapsto a$, $1\mapsto b$.$$
Lean4
/-- This is the order isomorphism from `Fin 2` to a finset `{a, b}` when `a < b`. -/
noncomputable def orderIsoPair : Fin 2 ≃o ({ a, b } : Finset α) :=
StrictMono.orderIsoOfSurjective ![⟨a, by simp⟩, ⟨b, by simp⟩] (strictMono_vecEmpty.vecCons hab)
(fun ⟨x, hx⟩ ↦ by
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
obtain rfl | rfl := hx
· exact ⟨0, rfl⟩
· exact ⟨1, rfl⟩)
