ker_mk_eq

Mathlib.Data.Setoid.Basic

URI: https://scilib.ai/kg/mathlib#Setoid.ker_mk_eq

← MathLib Explorer

English

The kernel of the quotient map mk'' is exactly the Setoid r.

Русский

Кернел отображения Quotient.mk'' равен relation r.

LaTeX

$$$ \ker(\,\operatorname{Quotient.mk''}\,)=r $$$

Lean4

/-- The kernel of the quotient map induced by an equivalence relation r equals r. -/
@[simp]
theorem ker_mk_eq (r : Setoid α) : ker (@Quotient.mk'' _ r) = r :=
  ext fun _ _ => Quotient.eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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