lift'_mk

Mathlib.Topology.UniformSpace.Separation

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.lift'_mk

English

For a T0-space β and f: α → β, lift' f behaves as f on representative mk a.

Русский

Для T0-пространства β и отображения f: α → β, lift' f совпадает с f на представителе mk a.

LaTeX

$$$\text{lift'} f (\mathrm{mk} a) = f a$$$

Lean4

theorem lift'_mk [T0Space β] {f : α → β} (h : UniformContinuous f) (a : α) : lift' f (mk a) = f a := by
  rw [lift', dif_pos h, lift_mk]

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

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

Разделы

Аффилиация

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