continuousOn_lift — Mathlib

English

ContinuousWithinAt (lift f hf) s (mk x) is equivalent to ContinuousWithinAt f (mk^{-1}' s) x.

Русский

ContinuousWithinAt (lift f hf) s (mk x) ⇔ ContinuousWithinAt f (mk^{-1}' s) x.

LaTeX

$$ContinuousWithinAt (lift f hf) s (mk x) ↔ ContinuousWithinAt f (Set.preimage mk s) x$$

Lean4

@[simp]
theorem continuousOn_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} :
    ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s) := by
  simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]

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