lift — Mathlib

English

There exists a lift of a function f : X → α to SeparationQuotient X → α, provided f is constant on inseparable pairs.

Русский

Существует продолжение функции $f$ на факторпространство SeparationQuotient X, если $f$ даёт одинаковые значения на инсепарируемых парах.

LaTeX

$$lift (f) (hf) : SeparationQuotient X → α where hf x y (x ~ᵢ y) ⇒ f x = f y$$

Lean4

/-- Lift a map `f : X → α` such that `Inseparable x y → f x = f y` to a map
`SeparationQuotient X → α`. -/
def lift (f : X → α) (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : SeparationQuotient X → α := fun x => Quotient.liftOn' x f hf

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