lift_surjective — Mathlib

English

If f is surjective, then the quotient lift (Quotient.lift f h) is surjective.

Русский

Если f сюръективно, то Quotient.lift f h сюръективно.

LaTeX

$$If $f$ is surjective, then $\\operatorname{Quotient.lift} f h$ is surjective.$$

Lean4

theorem lift_surjective {α β : Sort*} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b)
    (hf : Function.Surjective f) : Function.Surjective (Quotient.lift f h : Quotient s → β) :=
  (Quot.surjective_lift h).mpr hf

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