lift_mk — Mathlib

English

The universal property gives a map lift hf from T2Quotient X to Y for any continuous f.

Русский

Универсальное свойство дает отображение lift hf: T2Quotient X → Y для любой непрерывной f.

LaTeX

$$$ T2Quotient.lift hf : T2Quotient X \\to Y$$$

Lean4

@[simp]
theorem lift_mk {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f)
    (x : X) : lift hf (mk x) = f x :=
  Quotient.lift_mk (s := t2Setoid X) f (T2Quotient.compatible hf) x

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