range_quotient_mk'

Mathlib.Data.Set.Image

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

English

The range of Quotient.mk' is univ; the same as quotient.mk surjectivity.

Русский

Образ Quotient.mk' равен унив (всё множество).

LaTeX

$$$\operatorname{range}(\operatorname{Quotient.mk'} : \alpha \to \ Quotient s) = \mathrm{univ}$$$

Lean4

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

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

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

Разделы

Аффилиация

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