[GOAL]
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
  this.comp (MulOpposite.continuous_unop.prod_map continuous_id)
[GOAL]
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : SMul M X
inst✝² : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst✝¹ : SMul Mᵐᵒᵖ X
inst✝ : IsCentralScalar M X
⊢ Continuous fun p => MulOpposite.op p.fst • p.snd
[PROOFSTEP]
simpa only [op_smul_eq_smul] using (continuous_smul : Continuous fun p : M × X => _)
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
rw [← (@sInf_singleton _ _ ‹TopologicalSpace M› :)]
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ (t : TopologicalSpace X), t ∈ ts → ContinuousSMul M X
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
exact
  continuous_sInf_rng.2 fun t ht =>
    continuous_sInf_dom₂ (Eq.refl _) ht (@ContinuousSMul.continuous_smul _ _ _ _ t (h t ht))
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
refine' continuousSMul_iInf fun b => _
[GOAL]
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Sort u_1
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X
[PROOFSTEP]
assumption
[GOAL]
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ IsPreconnected Set.univ
[PROOFSTEP]
convert
  isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
    (continuous_id.vadd continuous_const).continuousOn
[GOAL]
case h.e'_3
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ Set.univ = ↑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ
[PROOFSTEP]
rw [Set.image_univ, Equiv.range_eq_univ]
