continuous_lift — Mathlib

English

There is a lift₂ of a bi-variable function f : X → Y → α to SeparationQuotient X → SeparationQuotient Y → α, provided f respects inseparability in both coordinates.

Русский

Существует двусторонний подъем функции f: X → Y → α к SeparationQuotient X → SeparationQuotient Y → α при условии совместного сохранения инсепарируемости.

LaTeX

$$lift₂ (f) hf : SeparationQuotient X → SeparationQuotient Y → α$$

Lean4

@[simp]
theorem continuous_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} : Continuous (lift f hf) ↔ Continuous f := by
  simp only [← continuousOn_univ, continuousOn_lift, preimage_univ]

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