range_quot_lift — Mathlib

English

If hf respects the equivalence relation, then the range of Quot.lift f hf equals the range of f.

Русский

Если hf сохраняет эквивалентность, то образ Quot.lift f hf совпадает с образом f.

LaTeX

$$$\operatorname{range}(\operatorname{Quot.lift} f hf) = \operatorname{range} f$$$

Lean4

@[simp]
theorem range_quot_lift {r : ι → ι → Prop} (hf : ∀ x y, r x y → f x = f y) : range (Quot.lift f hf) = range f :=
  ext fun _ => Quot.mk_surjective.exists

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