English
Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings, where the second embedding cannot take values in the range of the first.
Русский
Пары вложений с непересекающимися образами эквивалентны зависимой сумме вложений, в которой второе вложение не принимает значения из образа первого.
LaTeX
$$$\\{ f : (\\alpha \\hookrightarrow \\gamma) \\times (\\beta \\hookrightarrow \\gamma) \\;|\\; \\mathrm{Disjoint}(\\mathrm{range}(f.1), \\mathrm{range}(f.2)) \\} \\cong \\Sigma f : (\\alpha \\hookrightarrow \\gamma), \\beta \\hookrightarrow \\mathrm{⋃}(\\mathrm{range}(f))^c$$$
Lean4
/-- Pairs of embeddings with disjoint ranges are equivalent to a dependent sum of embeddings,
in which the second embedding cannot take values in the range of the first. -/
def prodEmbeddingDisjointEquivSigmaEmbeddingRestricted {α β γ : Type*} :
{ f : (α ↪ γ) × (β ↪ γ) // Disjoint (Set.range f.1) (Set.range f.2) } ≃ Σ f : α ↪ γ, β ↪ ↥(Set.range f)ᶜ :=
(subtypeProdEquivSigmaSubtype fun (a : α ↪ γ) (b : β ↪ _) => Disjoint (Set.range a) (Set.range b)).trans <|
Equiv.sigmaCongrRight fun a =>
(subtypeEquivProp <| by
ext f
rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]).trans
(codRestrict _ _)
