range_quotient_lift — Mathlib

English

For a setoid s, the range of Quot.lift f hf equals the range of f (lifted to the quotient).

Русский

Для множества по отношению эквивалентности s диапазон Quot.lift f hf равен диапазону f.

LaTeX

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

Lean4

@[simp]
theorem range_quotient_lift [s : Setoid ι] (hf) : range (Quotient.lift f hf : Quotient s → α) = range f :=
  range_quot_lift _

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