congr_arrowMap — Mathlib

English

Arrow maps congruent under MapEq coincide.

Русский

Стрелочные отображения совпадают при MapEq.

LaTeX

$$$ \\mathrm{congr\\_arrowMap} \\; iter_1 \\; iter_2 \\; h \\; h' $$$

Lean4

theorem congr_arrowMap {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h : k₁ ≤ k₂)
    (h₁ : k₂ ≤ j₁) (h₂ : k₂ ≤ j₂) : arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂ :=
  by
  wlog hj : j₁ ≤ j₂ generalizing j₁ j₂
  · simp [this iter₂ iter₁ h₂ h₁ ((not_le.1 hj).le)]
  rw [Subsingleton.elim iter₁ (iter₂.trunc hj)]
  rfl

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