English
If α1 ≃ α2 and γ ≃ δ, then the type of embeddings α1 ↪ γ is equivalent to the type of embeddings β ↪ δ when β ≃ α2 and δ ≃ γ respectively.
Русский
Если α1 ≃ α2 и γ ≃ δ, то множество вложений α1 ↪ γ эквивалентно множеству вложений β ↪ δ при соответствующих преобразованиях, где β ≃ α2 и δ ≃ γ.
LaTeX
$$$(\\alpha \\hookrightarrow \\gamma) \\simeq (\\beta \\hookrightarrow \\delta)$ при некоторых эквивалиентностях между парами (α,β) и (γ,δ)$$
Lean4
/-- If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then the type of embeddings `α₁ ↪ β₁`
is equivalent to the type of embeddings `α₂ ↪ β₂`. -/
@[simps apply]
def embeddingCongr {α β γ δ : Sort*} (h : α ≃ β) (h' : γ ≃ δ) : (α ↪ γ) ≃ (β ↪ δ)
where
toFun f := f.congr h h'
invFun f := f.congr h.symm h'.symm
left_inv
x := by
ext
simp
right_inv
x := by
ext
simp
