range_mk''

Mathlib.Data.Set.Image

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

English

The range of Quotient.mk'' (using a setoid sa) is univ; i.e., surjectivity of the double quotient map.

Русский

Образ Quotient.mk'' для набора sa охватывает всё множество.

LaTeX

$$$\operatorname{range}(\operatorname{Quotient.mk''} (s_\mathrm{a})) = \mathrm{univ}$$$

Lean4

theorem range_mk'' {sa : Setoid α} : range (Quotient.mk'' (s₁ := sa)) = univ :=
  range_quotient_mk

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

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

Разделы

Аффилиация

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