mapEq_trans — Mathlib

English

MapEq is transitive along a chain i1 ≤ i2 ≤ i3 with witnesses h12, h23.

Русский

MapEq транзитивна вдоль цепи i1 ≤ i2 ≤ i3 с доказательствами h12, h23.

LaTeX

$$$ \\text{MapEq } F G i_1 i_3 (h_{12}\\!:\\!i_1 \\le i_3) h_3 = \\text{(...) } $$$

Lean4

theorem mapEq_trans {i₁ i₂ i₃ : K} (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) {h₃ : i₃ ≤ x}
    (m₁₂ : MapEq F G i₁ i₂ h₁₂ (h₂₃.trans h₃)) (m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃) : MapEq F G i₁ i₃ (h₁₂.trans h₂₃) h₃ :=
  by
  simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]
  refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩
  rw [← homOfLE_comp (y := ⟨i₂, h₂₃.trans h₃⟩) h₁₂ h₂₃]
  simp [-homOfLE_comp, m₁₂.w, m₂₃.w]

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