snd_inj

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

English

If ac.Boundary i1 i2 and ac.Boundary i1' i2, then i1 = i1'.

Русский

Если ac.Boundary i1 i2 и ac.Boundary i1' i2, то i1 = i1'.

LaTeX

$$$ac.Boundary i_1 i_2 \land ac.Boundary i_1' i_2 \Rightarrow i_1 = i_1'.$$$

Lean4

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

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

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

Разделы

Аффилиация

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