isQuotientMap_quot_mk

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#isQuotientMap_quot_mk

English

The map Quot.mk r is a quotient map for any relation r on X.

Русский

Квартообразование Quot.mk r является квотируемым отображением для произвольного отношения r на X.

LaTeX

$$$\\text{IsQuotientMap}(\\text{Quot.mk } r).$$$

Lean4

theorem isQuotientMap_quot_mk : IsQuotientMap (@Quot.mk X r) :=
  ⟨Quot.exists_rep, rfl⟩

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

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

Разделы

Аффилиация

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