mk_eq_mk

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.mk_eq_mk

English

mk x = mk y iff x ~ᵢ y.

Русский

mk(x) = mk(y) эквивалентно x ~ᵢ y.

LaTeX

$$$\\mathrm{mk}(x) = \\mathrm{mk}(y) \\iff x \\sim_i y.$$$

Lean4

@[simp]
theorem mk_eq_mk : mk x = mk y ↔ (x ~ᵢ y) :=
  Quotient.eq''

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

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

Разделы

Аффилиация

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