fst_inj

Mathlib.Algebra.Homology.Embedding.AreComplementary

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.AreComplementary.Boundary.fst_inj

English

Equations for fromSum on the right injection: fromSum(Sum.inr i2) = e2.f i2.

Русский

Уравнение для fromSum по правой инъекции: fromSum(Sum.inr i2) = e2.f i2.

LaTeX

$$$\mathrm{fromSum}(\mathrm{Sum.inr}(i_2)) = e_2.f(i_2).$$$

Lean4

theorem fst_inj {i₁ i₁' : ι₁} {i₂ : ι₂} (h : ac.Boundary i₁ i₂) (h' : ac.Boundary i₁' i₂) : i₁ = i₁' :=
  e₁.injective_f (c.prev_eq h h')

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

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

Разделы

Аффилиация

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