orderIsoTriple — Mathlib

English

There is an order isomorphism Fin(3) ≃o {a,b,c} for a<b<c, sending 0→a, 1→b, 2→c.

Русский

Существует порядок-изоморфизм Fin(3) ≃o {a,b,c} при a<b<c, отображающий 0→a, 1→b, 2→c.

LaTeX

$$$\mathrm{Fin}(3) \cong_o \{a,b,c\} \text{ when } a

Lean4

/-- This is the order isomorphism from `Fin 3`
to a finset `{a, b, c}` when `a < b` and `b < c`. -/
noncomputable def orderIsoTriple : Fin 3 ≃o ({ a, b, c } : Finset α) :=
  StrictMono.orderIsoOfSurjective ![⟨a, by simp⟩, ⟨b, by simp⟩, ⟨c, by simp⟩]
    (StrictMono.vecCons (strictMono_vecEmpty.vecCons hbc) hab)
    (fun ⟨x, hx⟩ ↦ by
      simp only [Finset.mem_insert, Finset.mem_singleton] at hx
      obtain rfl | rfl | rfl := hx
      · exact ⟨0, rfl⟩
      · exact ⟨1, rfl⟩
      · exact ⟨2, rfl⟩)

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