congr_f — Mathlib

English

Same as congr_f: equality of morphisms in Split implies equality of their f-components at index n.

Русский

То же самое, что congr_f: равенство стрелок в Split влечет равенство их компонент f_n.

LaTeX

$$$\forall \{S_1,S_2\}, \forall \{\Phi_1,\Phi_2\}, (\Phi_1 = \Phi_2) \Rightarrow (\Phi_1.f n = \Phi_2.f n)$$$

Lean4

theorem congr_f {S₁ S₂ : Split C} {Φ₁ Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) (n : ℕ) : Φ₁.f n = Φ₂.f n := by rw [h]

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