English
For any relation r on α, the quotient map Quot.mk r: α → Quotient r is surjective; thus its range is the entire quotient set.
Русский
Для любой эквивалентности r на α отображение к эквату Quot.mk r: α → Quotient r сюрьективно; следовательно, образ равен всему quotient.
LaTeX
$$$\operatorname{range}(\operatorname{Quot.mk} r) = \mathrm{univ}$$$
Lean4
@[simp]
theorem range_quot_mk (r : α → α → Prop) : range (Quot.mk r) = univ :=
Quot.mk_surjective.range_eq