X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type ?u.110528
ι : Type ?u.110531
π : ι → Type ?u.110536
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ (fun x => (mk x.fst, mk x.snd)) ⁻¹' s →
        ContinuousWithinAt (uncurry f) ((fun x => (mk x.fst, mk x.snd)) ⁻¹' s) (a, b)
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type ?u.110528
ι : Type ?u.110531
π : ι → Type ?u.110536
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (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)
simp_rw [ContinuousOn, (surjective_mk.Prod_map surjective_mk).forall, Prod.forall, Prod.map,
  continuousWithinAt_lift₂]
no goals
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type ?u.110528
ι : Type ?u.110531
π : ι → Type ?u.110536
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s✝ : Set X
f✝ : X → Y
t : Set (SeparationQuotient X)
f : X → Y → Z
hf : ∀ (a : X) (b : Y) (c : X) (d : Y), (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d
s : Set (SeparationQuotient X × SeparationQuotient Y)
⊢ (∀ (a : X) (b : Y), (mk a, mk b) ∈ s → ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (a, b)) ↔
    ∀ (a : X) (b : Y),
      (a, b) ∈ (fun x => (mk x.fst, mk x.snd)) ⁻¹' s →
        ContinuousWithinAt (uncurry f) ((fun x => (mk x.fst, mk x.snd)) ⁻¹' s) (a, b)
rfl