English
The surjectivity of Quot.lift f h is equivalent to the surjectivity of f, provided h is compatible with r.
Русский
Суръективность Quot.lift f h эквивалентна сурьективности f при условии совместимости h с relation r.
LaTeX
$$$$\forall {\alpha : Sort*} {\gamma : Sort*} {r : α \to α \to Prop} {f : α \to \gamma} (h : ∀ (a1 a2 : α), r a1 a2 \to f a1 = f a2),\n Iff (Function.Surjective (Quot.lift f h)) (Function.Surjective f).$$$$
Lean4
@[simp]
theorem surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
Function.Surjective (lift f h) ↔ Function.Surjective f :=
⟨fun hf => hf.comp Quot.exists_rep, fun hf y =>
let ⟨x, hx⟩ := hf y;
⟨Quot.mk _ x, hx⟩⟩
