equivOfSurjective — Mathlib

English

Convert a surjective embedding f: α ↪ β into an equivalence α ≃ β.

Русский

Преобразовать сюръективное вложение f: α ↪ β в эквиваленцию α ≃ β.

LaTeX

$$$f : \\alpha \\hookrightarrow \\beta\\quad hf : \\text{Surjective} f\\;\\Rightarrow\\; \\mathrm{equivOfSurjective}(f,hf) : \\alpha \\simeq \\beta$$$

Lean4

/-- Convert a surjective `Embedding` to an `Equiv` -/
protected noncomputable def equivOfSurjective {α β} (f : α ↪ β) (hf : Surjective f) : α ≃ β :=
  Equiv.ofBijective f ⟨f.injective, hf⟩

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