surjective_liftOn' — Mathlib

English

For a function f and liftOn' f h, surjectivity of the lifted function is equivalent to surjectivity of f.

Русский

Для функции f и отображения liftOn' f h сюръективность поднятой функции равна сюръективности f.

LaTeX

$$$\\operatorname{Surjective}(\\lambda x:\\, \\operatorname{Quotient}(s_1) \\mapsto x.liftOn' f h) \\iff \\operatorname{Surjective}(f)$$$

Lean4

@[simp]
theorem surjective_liftOn' {f : α → φ} (h) :
    Function.Surjective (fun x : Quotient s₁ ↦ x.liftOn' f h) ↔ Function.Surjective f :=
  Quot.surjective_lift _

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