English
Transfer an embedding along a pair of equivalences: given e1: α ≃ β, e2: γ ≃ δ and f: α ↪ γ, produce an embedding β ↪ δ.
Русский
Перенос вложения вдоль пары эквиваленций: даны e1: α ≃ β, e2: γ ≃ δ и f: α ↪ γ; получаемое вложение β ↪ δ.
LaTeX
$$$\\mathrm{congr}(e_1,e_2,f) : \\beta \\hookrightarrow \\delta \\,=\\, (e_1^{ -1})\\,\\operatorname{toEmbedding}\\; (f) \\;\\operatorname{toEmbedding}\\; e_2$$$
Lean4
/-- Transfer an embedding along a pair of equivalences. -/
@[simps! -fullyApplied +simpRhs]
protected def congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (f : α ↪ γ) : β ↪ δ :=
(Equiv.toEmbedding e₁.symm).trans (f.trans e₂.toEmbedding)
