continuousOn_lift₂ — Mathlib

English

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

Русский

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

LaTeX

$$ContinuousOn (Function.uncurry (SeparationQuotient.lift f hf)) s ↔ ContinuousOn (Function.uncurry f) (Set.preimage (Prod.map SeparationQuotient.mk SeparationQuotient.mk) s)$$

Lean4

@[simp]
theorem continuousOn_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {s : Set (SeparationQuotient X × SeparationQuotient Y)} :
    ContinuousOn (uncurry <| lift₂ f hf) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s) :=
  by
  simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map, continuousWithinAt_lift₂]
  rfl

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