equiv_inl

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

English

For i1 in ι1 and i2 in ι2, ac.equiv(Sum.inl i1) = e1.f i1 and ac.equiv(Sum.inr i2) = e2.f i2.

Русский

Для элементов i1 из ι1 и i2 из ι2 выполнено: ac.equiv(Sum.inl i1) = e1.f(i1) и ac.equiv(Sum.inr i2) = e2.f(i2).

LaTeX

$$$ac.equiv(\mathrm{Sum.inl}(i_1)) = e_1.f(i_1),\; ac.equiv(\mathrm{Sum.inr}(i_2)) = e_2.f(i_2).$$$

Lean4

@[simp]
theorem equiv_inl (i₁ : ι₁) : ac.equiv (Sum.inl i₁) = e₁.f i₁ :=
  rfl

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

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

Разделы

Аффилиация

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