range_quotient_lift_on' — Mathlib

English

For a setoid s, the range of the liftOn' construction equals the range of f.

Русский

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

LaTeX

$$$\operatorname{range}(\lambda x : Quotient s, x.liftOn' f hf) = \operatorname{range} f$$$

Lean4

@[simp]
theorem range_quotient_lift_on' {s : Setoid ι} (hf) : (range fun x : Quotient s => Quotient.liftOn' x f hf) = range f :=
  range_quot_lift _

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