instFintype — Mathlib

English

Extensionality principle for II-indexed Splitting: if A1.fst = A2.fst and the pulled e-components agree, then A1 = A2.

Русский

Экстенсиальность для II-индексированных разбиений: если A1.fst = A2.fst и компоненты e согласованы через вытяжку, то A1 = A2.

LaTeX

$$$A_1 = A_2 \\;\\Rightarrow\\; A_1.fst = A_2.fst \\land A_1.e = A_2.e$$$

Lean4

instance : Fintype (IndexSet Δ) :=
  Fintype.ofInjective
    (fun A => ⟨⟨A.1.unop.len, Nat.lt_succ_iff.mpr (len_le_of_epi A.e)⟩, A.e.toOrderHom⟩ :
      IndexSet Δ → Sigma fun k : Fin (Δ.unop.len + 1) => Fin (Δ.unop.len + 1) → Fin (k + 1))
    (by
      rintro ⟨⟨Δ₁⟩, α₁⟩ ⟨⟨Δ₂⟩, α₂⟩ h₁
      simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
      have h₂ : Δ₁ = Δ₂ := by
        ext1
        simpa only [Fin.mk_eq_mk] using h₁.1
      subst h₂
      refine ext _ _ rfl ?_
      ext : 2
      exact eq_of_heq h₁.2)

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