fromSum — Mathlib

English

Given complementary embeddings e1 and e2, there is a canonical bijection ac.equiv between the disjoint sum ι1 ⊕ ι2 and ι.

Русский

При наличии комплементарных вложений e1 и e2 существует каноническая биекция ac.equiv между расщеплённой суммой индексов ι1 ⊕ ι2 и ι.

LaTeX

$$$ac.equiv : (\iota_1 \oplus \iota_2) \simeq \iota,$ где $ac$ задаётся как биекция через $fromSum_bijective$.$$

Lean4

/-- Given complementary embeddings of complex shapes
`e₁ : Embedding c₁ c` and `e₂ : Embedding c₂ c`, this is
the obvious map `ι₁ ⊕ ι₂ → ι` from the sum of the index
types of `c₁` and `c₂` to the index type of `c`. -/
@[simp]
def fromSum : ι₁ ⊕ ι₂ → ι
  | Sum.inl i₁ => e₁.f i₁
  | Sum.inr i₂ => e₂.f i₂

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