snd

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

English

Equations for fromSum on the left injection: fromSum(Sum.inl i1) = e1.f i1.

Русский

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

LaTeX

$$$\mathrm{fromSum}(\mathrm{Sum.inl}(i_1)) = e_1.f(i_1).$$$

Lean4

theorem snd : e₂.BoundaryGE i₂ :=
  e₂.boundaryGE h (fun _ => ac.symm.disjoint _ _)

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

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

Разделы

Аффилиация

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