[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ Continuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
rw [← Seminorm.coe_iSup_eq bdd]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ Continuous ↑(⨆ (i : ι), p i)
[PROOFSTEP]
refine Seminorm.continuous_of_lowerSemicontinuous _ ?_
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous ↑(⨆ (i : ι), p i)
[PROOFSTEP]
rw [Seminorm.coe_iSup_eq bdd]
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : BddAbove (range p)
⊢ LowerSemicontinuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
rw [Seminorm.bddAbove_range_iff] at bdd 
[GOAL]
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : ∀ (x : E), BddAbove (range fun i => ↑(p i) x)
⊢ LowerSemicontinuous (⨆ (i : ι), ↑(p i))
[PROOFSTEP]
convert lowerSemicontinuous_ciSup (f := fun i x ↦ p i x) bdd (fun i ↦ (hp i).lowerSemicontinuous)
[GOAL]
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : BarrelledSpace 𝕜 E
p : ι → Seminorm 𝕜 E
hp : ∀ (i : ι), Continuous ↑(p i)
bdd : ∀ (x : E), BddAbove (range fun i => ↑(p i) x)
x✝ : E
⊢ iSup (fun i => ↑(p i)) x✝ = ⨆ (i : ι), ↑(p i) x✝
[PROOFSTEP]
exact iSup_apply
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
⊢ ∀ (p : Seminorm 𝕜₁ E), LowerSemicontinuous ↑p → Continuous ↑p
[PROOFSTEP]
intro p hp
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
⊢ Continuous ↑p
[PROOFSTEP]
have h₁ : ∀ n : ℕ, IsClosed (p.closedBall (0 : E) n) := fun n ↦ by
  simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
n : ℕ
⊢ IsClosed (Seminorm.closedBall p 0 ↑n)
[PROOFSTEP]
simpa [p.closedBall_zero_eq] using hp.isClosed_preimage n
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
⊢ Continuous ↑p
[PROOFSTEP]
have h₂ : (⋃ n : ℕ, p.closedBall (0 : E) n) = univ :=
  eq_univ_of_forall fun x ↦
    mem_iUnion.mpr
      (exists_nat_ge <| p (x - 0))
        -- Hence, one of them has nonempty interior. Let `n : ℕ` be its radius, and fix `x` an
            -- interior point.
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
⊢ Continuous ↑p
[PROOFSTEP]
rcases nonempty_interior_of_iUnion_of_closed h₁ h₂ with
  ⟨n, ⟨x, hxn⟩⟩
    -- To show that `p` is continuous, we will show that the `p`-closed-ball of
        -- radius `2*n` is a neighborhood of zero.
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior (Seminorm.closedBall p 0 ↑n)
⊢ Continuous ↑p
[PROOFSTEP]
refine Seminorm.continuous' (r := n + n) ?_
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior (Seminorm.closedBall p 0 ↑n)
⊢ Seminorm.closedBall p 0 (↑n + ↑n) ∈ 𝓝 0
[PROOFSTEP]
rw [p.closedBall_zero_eq] at hxn ⊢
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
have hxn' : p x ≤ n := by convert interior_subset hxn
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
⊢ ↑p x ≤ ↑n
[PROOFSTEP]
convert interior_subset hxn
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn : x ∈ interior {y | ↑p y ≤ ↑n}
hxn' : ↑p x ≤ ↑n
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds, ← map_add_left_nhds_zero] at hxn 
[GOAL]
case intro.intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
⊢ {y | ↑p y ≤ ↑n + ↑n} ∈ 𝓝 0
[PROOFSTEP]
filter_upwards [hxn] with y hy
[GOAL]
case h
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' {y | ↑p y ≤ ↑n}
⊢ ↑p y ≤ ↑n + ↑n
[PROOFSTEP]
calc
  p y = p (x + y - x) := by rw [add_sub_cancel']
  _ ≤ p (x + y) + p x := (map_sub_le_add _ _ _)
  _ ≤ n + n := add_le_add hy hxn'
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹¹ : Nonempty κ
inst✝¹⁰ : NontriviallyNormedField 𝕜₁
inst✝⁹ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝⁸ : RingHomIsometric σ₁₂
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜₁ E
inst✝ : BaireSpace E
p : Seminorm 𝕜₁ E
hp : LowerSemicontinuous ↑p
h₁ : ∀ (n : ℕ), IsClosed (Seminorm.closedBall p 0 ↑n)
h₂ : ⋃ (n : ℕ), Seminorm.closedBall p 0 ↑n = univ
n : ℕ
x : E
hxn✝ : {y | ↑p y ≤ ↑n} ∈ 𝓝 x
hxn : {y | ↑p y ≤ ↑n} ∈ map ((fun x x_1 => x + x_1) x) (𝓝 0)
hxn' : ↑p x ≤ ↑n
y : E
hy : y ∈ (fun x_1 => x + x_1) ⁻¹' {y | ↑p y ≤ ↑n}
⊢ ↑p y = ↑p (x + y - x)
[PROOFSTEP]
rw [add_sub_cancel']
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
⊢ UniformEquicontinuous (FunLike.coe ∘ 𝓕)
[PROOFSTEP]
refine (hq.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup ((toLinearMap) ∘ 𝓕)).mpr ?_
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
⊢ ∀ (i : κ),
    BddAbove (range fun k => Seminorm.comp (q i) ((toLinearMap ∘ 𝓕) k)) ∧
      Continuous (⨆ (k : ι), ↑(Seminorm.comp (q i) ((toLinearMap ∘ 𝓕) k)))
[PROOFSTEP]
intro k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ BddAbove (range fun k_1 => Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous (⨆ (k_1 : ι), ↑(Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)))
[PROOFSTEP]
have : BddAbove (range fun i ↦ (q k).comp (𝓕 i).toLinearMap) :=
  by
  rw [Seminorm.bddAbove_range_iff]
  exact H k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ BddAbove (range fun i => Seminorm.comp (q k) ↑(𝓕 i))
[PROOFSTEP]
rw [Seminorm.bddAbove_range_iff]
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
⊢ ∀ (x : E), BddAbove (range fun i => ↑(Seminorm.comp (q k) ↑(𝓕 i)) x)
[PROOFSTEP]
exact H k
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁴ : Nonempty κ
inst✝¹³ : NontriviallyNormedField 𝕜₁
inst✝¹² : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹¹ : RingHomIsometric σ₁₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
inst✝⁶ : UniformSpace E
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup E
inst✝³ : UniformAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
H : ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(𝓕 i) x))
k : κ
this : BddAbove (range fun i => Seminorm.comp (q k) ↑(𝓕 i))
⊢ BddAbove (range fun k_1 => Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)) ∧
    Continuous (⨆ (k_1 : ι), ↑(Seminorm.comp (q k) ((toLinearMap ∘ 𝓕) k_1)))
[PROOFSTEP]
exact ⟨this, Seminorm.continuous_iSup _ (fun i ↦ (hq.continuous_seminorm k).comp (𝓕 i).continuous) this⟩
[GOAL]
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
⊢ Continuous (linearMapOfTendsto f (fun a => ↑(g a)) h).toAddHom.toFun
[PROOFSTEP]
rcases l.exists_seq_tendsto with
  ⟨u, hu⟩
    -- We claim that the limit is continuous because it's a limit of an equicontinuous family.
        -- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness.
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ Continuous (linearMapOfTendsto f (fun a => ↑(g a)) h).toAddHom.toFun
[PROOFSTEP]
refine (h.comp hu).continuous_of_equicontinuous_at (hq.banach_steinhaus ?_).equicontinuous
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
⊢ ∀ (k : κ) (x : E), BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
intro k x
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : Tendsto (fun n x => ↑(g n) x) l (𝓝 f)
u : ℕ → α
hu : Tendsto u atTop l
k : κ
x : E
⊢ BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
rw [tendsto_pi_nhds] at h 
[GOAL]
case intro
α : Type u_1
ι : Type u_2
κ : Type u_3
𝕜₁ : Type u_4
𝕜₂ : Type u_5
E : Type u_6
F : Type u_7
inst✝¹⁷ : Nonempty κ
inst✝¹⁶ : NontriviallyNormedField 𝕜₁
inst✝¹⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
inst✝¹⁴ : RingHomIsometric σ₁₂
inst✝¹³ : AddCommGroup E
inst✝¹² : AddCommGroup F
inst✝¹¹ : Module 𝕜₁ E
inst✝¹⁰ : Module 𝕜₂ F
inst✝⁹ : UniformSpace E
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup E
inst✝⁶ : UniformAddGroup F
inst✝⁵ : ContinuousSMul 𝕜₁ E
inst✝⁴ : ContinuousSMul 𝕜₂ F
inst✝³ : BarrelledSpace 𝕜₁ E
𝓕 : ι → E →SL[σ₁₂] F
q : SeminormFamily 𝕜₂ F κ
hq : WithSeminorms q
inst✝² : T2Space F
l : Filter α
inst✝¹ : IsCountablyGenerated l
inst✝ : NeBot l
g : α → E →SL[σ₁₂] F
f : E → F
h : ∀ (x : E), Tendsto (fun i => ↑(g i) x) l (𝓝 (f x))
u : ℕ → α
hu : Tendsto u atTop l
k : κ
x : E
⊢ BddAbove (range fun i => ↑(q k) (↑(g (u i)) x))
[PROOFSTEP]
exact (((hq.continuous_seminorm k).tendsto _).comp <| (h x).comp hu).bddAbove_range
