hom_ext

Mathlib.AlgebraicTopology.SimplicialObject.Split

URI: https://scilib.ai/kg/mathlib#SimplicialObject.Split.hom_ext

English

If Φ1 = Φ2, then their f-components are equal: Φ1.f = Φ2.f.

Русский

Если Φ1 = Φ2, то их компоненты f равны: Φ1.f = Φ2.f.

LaTeX

$$$\Phi_1 = \Phi_2 \Rightarrow \Phi_1.f = \Phi_2.f$$$

Lean4

@[ext]
theorem hom_ext {S₁ S₂ : Split C} (Φ₁ Φ₂ : S₁ ⟶ S₂) (h : ∀ n : ℕ, Φ₁.f n = Φ₂.f n) : Φ₁ = Φ₂ :=
  Hom.ext _ _ h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru