congr_F

Mathlib.AlgebraicTopology.SimplicialObject.Split

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

English

If Φ1 = Φ2, then their level-n components are equal: Φ1.f n = Φ2.f n for all n.

Русский

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

LaTeX

$$$\Phi_1 = \Phi_2 \Rightarrow \forall n, \Phi_1.f(n) = \Phi_2.f(n)$$$

Lean4

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

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

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

Разделы

Аффилиация

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