lift_surjective_iff — Mathlib

English

Let f : α → β satisfy h that f respects the Setoid relation. Then the quotient lift (Quotient.lift f h) is surjective if and only if f is surjective.

Русский

Пусть f : α → β сохраняет отношение эквивалентности, тогда отображение Quotient.lift f h сюръективно тогда и только тогда, когда f сюръективно.

LaTeX

$$$\\operatorname{Surjective}(\\operatorname{Quotient.lift} f h) \\iff \\operatorname{Surjective}(f)$$$

Lean4

@[simp]
theorem lift_surjective_iff {α β : Sort*} {s : Setoid α} (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) :
    Function.Surjective (Quotient.lift f h : Quotient s → β) ↔ Function.Surjective f :=
  Quot.surjective_lift h

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