ext — Mathlib

English

If two index-set elements A1 and A2 have the same fst component and their e-component matches under the appropriate transport, then A1 = A2.

Русский

Если два элемента индекса A1 и A2 имеют одинаковый первый компонент и их e-компоненты совпадают после переноса, то A1 = A2.

LaTeX

$$$A_1 = A_2$ при условии $A_1.1 = A_2.1$ и $A_1.e \\gg eqToHom(\\ldots) = A_2.e$$$

Lean4

theorem ext (A₁ A₂ : IndexSet Δ) (h₁ : A₁.1 = A₂.1) (h₂ : A₁.e ≫ eqToHom (by rw [h₁]) = A₂.e) : A₁ = A₂ :=
  by
  rcases A₁ with ⟨Δ₁, ⟨α₁, hα₁⟩⟩
  rcases A₂ with ⟨Δ₂, ⟨α₂, hα₂⟩⟩
  simp only at h₁
  subst h₁
  simp only [eqToHom_refl, comp_id, IndexSet.e] at h₂
  simp only [h₂]

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