hpath_hext — Mathlib

English

If two representative paths p1 and p2 are pointwise equal, then their path-homotopy quotient classes are HEq (heterogeneous equality).

Русский

Если два представителя путей совпадают по каждой точке, то их классы гомотопии в факторе равны через HEq.

LaTeX

$$$\text{If } \forall t:\, p_1(t)=p_2(t)\text{, then } ⟦p_1⟧ =_{HEq} ⟦p_2⟧.$$$

Lean4

theorem hpath_hext {p₁ : Path x₀ x₁} {p₂ : Path x₂ x₃} (hp : ∀ t, p₁ t = p₂ t) :
    HEq (α := Path.Homotopic.Quotient _ _) ⟦p₁⟧ (β := Path.Homotopic.Quotient _ _) ⟦p₂⟧ :=
  by
  obtain rfl : x₀ = x₂ := by convert hp 0 <;> simp
  obtain rfl : x₁ = x₃ := by convert hp 1 <;> simp
  rw [heq_iff_eq]; congr; ext t; exact hp t

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