lift_comp_mk

Mathlib.Topology.Inseparable

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

English

The lift composed with mk equals the original function: lift f hf ∘ mk = f.

Русский

Состав lift f hf с mk равен исходной функции: lift f hf ∘ mk = f.

LaTeX

$$lift f hf ∘ mk = f$$

Lean4

@[simp]
theorem lift_comp_mk {f : X → α} (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : lift f hf ∘ mk = f :=
  rfl

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

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

Разделы

Аффилиация

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