mk_comp_outCLM

Mathlib.Topology.Algebra.SeparationQuotient.Section

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

English

The composition of mk with outCLM equals the identity on SeprationQuotient E.

Русский

Составление mk ∘ outCLM равно тождественному отображению на SeparationQuotient E.

LaTeX

$$$\mathrm{mk} \circ outCLM = \mathrm{id}$$$

Lean4

@[simp]
theorem mk_comp_outCLM : mk ∘ outCLM K E = id :=
  funext (mk_outCLM K)

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

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

Разделы

Аффилиация

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