English
Equivalence between embeddings from a sum α ⊕ β into γ and a dependent pair consisting of an embedding α ↪ γ and a β ↪ ↥(Set.range f)ᶜ, i.e., into the complement of the image of the first embedding.
Русский
Эквивалентность между вложениями из суммы α ⊕ β в γ и зависимой парой, состоящей из вложения α ⊂ γ и вложения β в допуск к дополнению образа первого вложения.
LaTeX
$$$ (α ⊕ β) ↪ γ \\cong Σ f : α ↪ γ, β ↪ ↥(Set.range f)^{c} $$$
Lean4
/-- A combination of the above results, allowing us to turn one embedding over a sum type
into two dependent embeddings, the second of which avoids any members of the range
of the first. This is helpful for constructing larger embeddings out of smaller ones. -/
def sumEmbeddingEquivSigmaEmbeddingRestricted {α β γ : Type*} : (α ⊕ β ↪ γ) ≃ Σ f : α ↪ γ, β ↪ ↥(Set.range f)ᶜ :=
Equiv.trans sumEmbeddingEquivProdEmbeddingDisjoint prodEmbeddingDisjointEquivSigmaEmbeddingRestricted
