mk_surjective

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#Quot.mk_surjective

English

Quot.mk r is a surjective function: every quotient class has a representative.

Русский

Quot.mk r является сюръективной функцией: каждый класс эквивалентности имеет представителя.

LaTeX

$$$\\mathrm{Surjective}(\\mathrm{Quot.mk} r)$$$

Lean4

/-- `Quot.mk r` is a surjective function. -/
theorem mk_surjective {r : α → α → Prop} : Function.Surjective (Quot.mk r) :=
  Quot.exists_rep

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

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

Разделы

Аффилиация

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