range_quotient_mk

Mathlib.Data.Set.Image

URI: https://scilib.ai/kg/mathlib#Set.range_quotient_mk

English

The range of Quotient.mk r is the entire quotient type; same fact as Quot.mk surjectivity.

Русский

Образ Quotient.mk r равен всему типу Quotient r; то же утверждение про сюрьективность.

LaTeX

$$$\operatorname{range}(\operatorname{Quotient.mk} r) = \mathrm{univ}$$$

Lean4

@[simp]
theorem range_quotient_mk {s : Setoid α} : range (Quotient.mk s) = univ :=
  range_quot_mk _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru