ext — Mathlib

English

Another extensionality statement for paths: equality of the underlying functions implies equality of paths.

Русский

Еще одно утверждение о расширении путей: равенство соответствующих функций означает равенство путей.

LaTeX

$$$\forall \gamma_1, \gamma_2 : Path\ x\ y, (\gamma_1 : I \to X) = (\gamma_2 : I \to X) \Rightarrow \gamma_1 = \gamma_2$$$

Lean4

@[ext]
protected theorem ext : ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂ :=
  by
  rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
  rfl

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