desc'

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

English

There exists an equivalence between ι1 ⊕ ι2 and ι induced by AreComplementary.

Русский

Существует эквивелентность между ι1 ⊕ ι2 и ι, индукированная AreComplementary.

LaTeX

$$$\exists\text{Equiv } ac.equiv : (ι_1 \oplus ι_2) \simeq ι.$$$

Lean4

/-- Auxiliary definition for `desc`. -/
def desc' : ∀ (i : ι₁ ⊕ ι₂), X (ac.equiv i)
  | Sum.inl i₁ => x₁ i₁
  | Sum.inr i₂ => x₂ i₂

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

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

Разделы

Аффилиация

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