equiv — Mathlib

English

The equivalence ac.equiv is defined by the bijection fromSum_bijective associated to AreComplementary.

Русский

Равносвязка ac.equiv задаётся биекцией, полученной из fromSum_bijective, связанной с AreComplementary.

LaTeX

$$$ac.equiv : (\iota_1 \oplus \iota_2) \simeq \iota \text{ is defined by } ac.fromSum_bijective.$$$

Lean4

/-- Given complementary embeddings of complex shapes
`e₁ : Embedding c₁ c` and `e₂ : Embedding c₂ c`, this is
the obvious bijection `ι₁ ⊕ ι₂ ≃ ι` from the sum of the index
types of `c₁` and `c₂` to the index type of `c`. -/
noncomputable def equiv : ι₁ ⊕ ι₂ ≃ ι :=
  Equiv.ofBijective _ (ac.fromSum_bijective)

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