[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ strongTopology σ F 𝔖 = UniformSpace.toTopologicalSpace
[PROOFSTEP]
rw [strongTopology, UniformAddGroup.toUniformSpace_eq]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced FunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) = UniformSpace.toTopologicalSpace
[PROOFSTEP]
rfl
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
rw [strongUniformity, UniformSpace.replaceTopology_eq]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
let φ : (E →SL[σ] F) →+ E →ᵤ[𝔖] F := ⟨⟨(FunLike.coe : (E →SL[σ] F) → E →ᵤ[𝔖] F), rfl⟩, fun _ _ => rfl⟩
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
φ : (E →SL[σ] F) →+ E →ᵤ[𝔖] F :=
  { toZeroHom := { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) },
    map_add' :=
      (_ :
        ∀ (x x_1 : E →SL[σ] F),
          ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1) =
            ZeroHom.toFun { toFun := FunLike.coe, map_zero' := (_ : ↑0 = ↑0) } (x + x_1)) }
⊢ UniformAddGroup (E →SL[σ] F)
[PROOFSTEP]
exact uniformAddGroup_comap φ
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup (E →SL[σ] F) := strongUniformity.uniformAddGroup σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
𝔖 : Set (Set E)
this✝² : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝¹ : UniformAddGroup F
this✝ : UniformSpace (E →SL[σ] F) := strongUniformity σ F 𝔖
this : UniformAddGroup (E →SL[σ] F)
⊢ TopologicalAddGroup (E →SL[σ] F)
[PROOFSTEP]
infer_instance
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
haveI : T2Space (E →ᵤ[𝔖] F) := UniformOnFun.t2Space_of_covering h𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁴ : NormedField 𝕜₁
inst✝¹³ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹² : AddCommGroup E
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : AddCommGroup E'
inst✝⁹ : Module ℝ E'
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : AddCommGroup F'
inst✝⁵ : Module ℝ F'
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace E'
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : T2Space F
𝔖 : Set (Set E)
h𝔖 : ⋃₀ 𝔖 = Set.univ
this✝² : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝¹ : UniformAddGroup F
this✝ : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
this : T2Space (E →ᵤ[𝔖] F)
⊢ T2Space (E →SL[σ] F)
[PROOFSTEP]
exact (strongTopology.embedding_coeFn σ F 𝔖).t2Space
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
let φ : (E →SL[σ] F) →ₗ[𝕜₂] E →ᵤ[𝔖] F := ⟨⟨(FunLike.coe : (E →SL[σ] F) → E → F), fun _ _ => rfl⟩, fun _ _ => rfl⟩
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹⁶ : NormedField 𝕜₁
inst✝¹⁵ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : Module 𝕜₁ E
inst✝¹² : AddCommGroup E'
inst✝¹¹ : Module ℝ E'
inst✝¹⁰ : AddCommGroup F
inst✝⁹ : Module 𝕜₂ F
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module ℝ F'
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace E'
inst✝⁴ : RingHomSurjective σ
inst✝³ : RingHomIsometric σ
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul 𝕜₂ F
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
h𝔖₃ : ∀ (S : Set E), S ∈ 𝔖 → Bornology.IsVonNBounded 𝕜₁ S
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
φ : (E →SL[σ] F) →ₗ[𝕜₂] E →ᵤ[𝔖] F :=
  { toAddHom := { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_1 : E →SL[σ] F), ↑(x + x_1) = ↑(x + x_1)) },
    map_smul' :=
      (_ :
        ∀ (x : 𝕜₂) (x_1 : E →SL[σ] F),
          AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_2 : E →SL[σ] F), ↑(x + x_2) = ↑(x + x_2)) }
              (x • x_1) =
            AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (x x_2 : E →SL[σ] F), ↑(x + x_2) = ↑(x + x_2)) }
              (x • x_1)) }
⊢ ContinuousSMul 𝕜₂ (E →SL[σ] F)
[PROOFSTEP]
exact
  UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜₂ E F (E →SL[σ] F) h𝔖₁ h𝔖₂ φ ⟨rfl⟩ fun u s hs =>
    (h𝔖₃ s hs).image u
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
letI : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ Filter.HasBasis (𝓝 0) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn σ F 𝔖).toInducing.nhds_eq_comap]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹³ : NormedField 𝕜₁
inst✝¹² : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
E' : Type u_4
F : Type u_5
F' : Type u_6
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜₁ E
inst✝⁹ : AddCommGroup E'
inst✝⁸ : Module ℝ E'
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : AddCommGroup F'
inst✝⁴ : Module ℝ F'
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace E'
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalAddGroup F
ι : Type u_7
𝔖 : Set (Set E)
h𝔖₁ : Set.Nonempty 𝔖
h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
b : ι → Set F
h : Filter.HasBasis (𝓝 0) p b
this✝¹ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this✝ : UniformAddGroup F
this : TopologicalSpace (E →SL[σ] F) := strongTopology σ F 𝔖
⊢ Filter.HasBasis (Filter.comap (↑(UniformOnFun.ofFun 𝔖) ∘ FunLike.coe) (𝓝 ((↑(UniformOnFun.ofFun 𝔖) ∘ FunLike.coe) 0)))
    (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => {f | ∀ (x : E), x ∈ Si.fst → ↑f x ∈ b Si.snd}
[PROOFSTEP]
exact (UniformOnFun.hasBasis_nhds_zero_of_basis 𝔖 h𝔖₁ h𝔖₂ h).comap FunLike.coe
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp f L,
              map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
          map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn _ _ _).continuous_iff]
  -- Porting note: without this, the following doesn't work
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    ((↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ FunLike.coe) ∘
      {
            toAddHom :=
              { toFun := fun f => comp f L,
                map_add' := (_ : ∀ (f g : F →SL[τ] G), comp (f + g) L = comp f L + comp g L) },
            map_smul' := (_ : ∀ (a : 𝕜₃) (f : F →SL[τ] G), comp (a • f) L = a • comp f L) }.toAddHom.toFun)
[PROOFSTEP]
change Continuous ((λ f ↦ UniformOnFun.ofFun _ (f ∘ L)) ∘ FunLike.coe)
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup G
inst✝² : ContinuousConstSMul 𝕜₃ G
inst✝¹ : RingHomSurjective σ
inst✝ : RingHomIsometric σ
L : E →SL[σ] F
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous ((fun f => ↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) (f ∘ ↑L)) ∘ FunLike.coe)
[PROOFSTEP]
exact
  (UniformOnFun.precomp_uniformContinuous fun S hS => hS.image L).continuous.comp
    (strongTopology.embedding_coeFn _ _ _).continuous
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace G := TopologicalAddGroup.toUniformSpace G
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this : UniformSpace G := TopologicalAddGroup.toUniformSpace G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup G := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this : UniformAddGroup G
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
letI : UniformSpace F := TopologicalAddGroup.toUniformSpace F
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝¹ : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝ : UniformAddGroup G
this : UniformSpace F := TopologicalAddGroup.toUniformSpace F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
haveI : UniformAddGroup F := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝¹ : UniformAddGroup G
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous
    {
          toAddHom :=
            { toFun := fun f => comp L f,
              map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
          map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun
[PROOFSTEP]
rw [(strongTopology.embedding_coeFn _ _ _).continuous_iff]
[GOAL]
𝕜₁ : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
inst✝²⁰ : NormedField 𝕜₁
inst✝¹⁹ : NormedField 𝕜₂
inst✝¹⁸ : NormedField 𝕜₃
σ : 𝕜₁ →+* 𝕜₂
τ : 𝕜₂ →+* 𝕜₃
ρ : 𝕜₁ →+* 𝕜₃
inst✝¹⁷ : RingHomCompTriple σ τ ρ
E : Type u_4
E' : Type u_5
F : Type u_6
F' : Type u_7
G : Type u_8
inst✝¹⁶ : AddCommGroup E
inst✝¹⁵ : Module 𝕜₁ E
inst✝¹⁴ : AddCommGroup E'
inst✝¹³ : Module ℝ E'
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₂ F
inst✝¹⁰ : AddCommGroup F'
inst✝⁹ : Module ℝ F'
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜₃ G
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalAddGroup F
inst✝² : TopologicalAddGroup G
inst✝¹ : ContinuousConstSMul 𝕜₃ G
inst✝ : ContinuousConstSMul 𝕜₂ F
L : F →SL[τ] G
this✝² : UniformSpace G := TopologicalAddGroup.toUniformSpace G
this✝¹ : UniformAddGroup G
this✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F
this : UniformAddGroup F
⊢ Continuous
    ((↑(UniformOnFun.ofFun {S | Bornology.IsVonNBounded 𝕜₁ S}) ∘ FunLike.coe) ∘
      {
            toAddHom :=
              { toFun := fun f => comp L f,
                map_add' := (_ : ∀ (f₁ f₂ : E →SL[σ] F), comp L (f₁ + f₂) = comp L f₁ + comp L f₂) },
            map_smul' := (_ : ∀ (c : 𝕜₂) (f : E →SL[σ] F), comp L (c • f) = ↑τ c • comp L f) }.toAddHom.toFun)
[PROOFSTEP]
exact
  (UniformOnFun.postcomp_uniformContinuous L.uniformContinuous).continuous.comp
    (strongTopology.embedding_coeFn _ _ _).continuous
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
𝕜₄ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝³¹ : AddCommGroup E
inst✝³⁰ : AddCommGroup F
inst✝²⁹ : AddCommGroup G
inst✝²⁸ : AddCommGroup H
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : NontriviallyNormedField 𝕜₂
inst✝²⁵ : NontriviallyNormedField 𝕜₃
inst✝²⁴ : NontriviallyNormedField 𝕜₄
inst✝²³ : Module 𝕜 E
inst✝²² : Module 𝕜₂ F
inst✝²¹ : Module 𝕜₃ G
inst✝²⁰ : Module 𝕜₄ H
inst✝¹⁹ : TopologicalSpace E
inst✝¹⁸ : TopologicalSpace F
inst✝¹⁷ : TopologicalSpace G
inst✝¹⁶ : TopologicalSpace H
inst✝¹⁵ : TopologicalAddGroup G
inst✝¹⁴ : TopologicalAddGroup H
inst✝¹³ : ContinuousConstSMul 𝕜₃ G
inst✝¹² : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₁
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
src✝ : (E →SL[σ₁₄] H) ≃ (F →SL[σ₂₃] G) := arrowCongrEquiv e₁₂ e₄₃
f g : E →SL[σ₁₄] H
⊢ (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) (f + g) =
    (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) f +
      (fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂))) g
[PROOFSTEP]
simp only [add_comp, comp_add]
[GOAL]
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type u_3
𝕜₄ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
inst✝³¹ : AddCommGroup E
inst✝³⁰ : AddCommGroup F
inst✝²⁹ : AddCommGroup G
inst✝²⁸ : AddCommGroup H
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : NontriviallyNormedField 𝕜₂
inst✝²⁵ : NontriviallyNormedField 𝕜₃
inst✝²⁴ : NontriviallyNormedField 𝕜₄
inst✝²³ : Module 𝕜 E
inst✝²² : Module 𝕜₂ F
inst✝²¹ : Module 𝕜₃ G
inst✝²⁰ : Module 𝕜₄ H
inst✝¹⁹ : TopologicalSpace E
inst✝¹⁸ : TopologicalSpace F
inst✝¹⁷ : TopologicalSpace G
inst✝¹⁶ : TopologicalSpace H
inst✝¹⁵ : TopologicalAddGroup G
inst✝¹⁴ : TopologicalAddGroup H
inst✝¹³ : ContinuousConstSMul 𝕜₃ G
inst✝¹² : ContinuousConstSMul 𝕜₄ H
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
σ₃₄ : 𝕜₃ →+* 𝕜₄
σ₄₃ : 𝕜₄ →+* 𝕜₃
σ₂₄ : 𝕜₂ →+* 𝕜₄
σ₁₄ : 𝕜 →+* 𝕜₄
inst✝¹¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝¹⁰ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝⁷ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁶ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝³ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝² : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₁
e₁₂ : E ≃SL[σ₁₂] F
e₄₃ : H ≃SL[σ₄₃] G
src✝ : (E →SL[σ₁₄] H) ≃ (F →SL[σ₂₃] G) := arrowCongrEquiv e₁₂ e₄₃
t : 𝕜₄
f : E →SL[σ₁₄] H
⊢ AddHom.toFun
      { toFun := fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂)),
        map_add' :=
          (_ :
            ∀ (f g : E →SL[σ₁₄] H),
              comp (↑e₄₃) (comp (f + g) ↑(ContinuousLinearEquiv.symm e₁₂)) =
                comp (↑e₄₃) (comp f ↑(ContinuousLinearEquiv.symm e₁₂)) +
                  comp (↑e₄₃) (comp g ↑(ContinuousLinearEquiv.symm e₁₂))) }
      (t • f) =
    ↑σ₄₃ t •
      AddHom.toFun
        { toFun := fun L => comp (↑e₄₃) (comp L ↑(ContinuousLinearEquiv.symm e₁₂)),
          map_add' :=
            (_ :
              ∀ (f g : E →SL[σ₁₄] H),
                comp (↑e₄₃) (comp (f + g) ↑(ContinuousLinearEquiv.symm e₁₂)) =
                  comp (↑e₄₃) (comp f ↑(ContinuousLinearEquiv.symm e₁₂)) +
                    comp (↑e₄₃) (comp g ↑(ContinuousLinearEquiv.symm e₁₂))) }
        f
[PROOFSTEP]
simp only [smul_comp, comp_smulₛₗ]
