case refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ i',
        (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
          {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 i

case refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ∀ (i' : Set E × ℝ),
    Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd →
      ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd}
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ContinuousLinearMap.tmpTopologicalSpace = topologicalSpace
refine'
  ContinuousLinearMap.tmpTopologicalAddGroup.ext inferInstance
    ((@Metric.nhds_basis_closedBall _ ContinuousLinearMap.tmpPseudoMetricSpace 0).ext
      (ContinuousLinearMap.hasBasis_nhds_zero_of_basis Metric.nhds_basis_closedBall) _ _)
case refine'_1.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ i',
        (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
          {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 i
case refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ i',
        (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
          {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 i
rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, hc₀, hc₁⟩
case refine'_1.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ ∃ i',
    (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
      {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 ε
case refine'_1.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
⊢ ∀ (i : ℝ),
    0 < i →
      ∃ i',
        (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
          {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 i
intro ε hε
case refine'_1.intro.intro.refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ Bornology.IsVonNBounded 𝕜 (closedBall 0 (1 / ‖c‖), ε).fst

case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ {f | ∀ (x : E), x ∈ (closedBall 0 (1 / ‖c‖), ε).fst → ↑f x ∈ closedBall 0 (closedBall 0 (1 / ‖c‖), ε).snd} ⊆
    closedBall 0 ε
case refine'_1.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ ∃ i',
    (Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd) ∧
      {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd} ⊆ closedBall 0 ε
refine' ⟨⟨closedBall 0 (1 / ‖c‖), ε⟩, ⟨⟨_, hε⟩, _⟩⟩
case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), x ∈ (closedBall 0 (1 / ‖c‖), ε).fst → ↑f x ∈ closedBall 0 (closedBall 0 (1 / ‖c‖), ε).snd
⊢ f ∈ closedBall 0 ε
case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ {f | ∀ (x : E), x ∈ (closedBall 0 (1 / ‖c‖), ε).fst → ↑f x ∈ closedBall 0 (closedBall 0 (1 / ‖c‖), ε).snd} ⊆
    closedBall 0 ε
intro f (hf : ∀ x, _)
case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
⊢ f ∈ closedBall 0 ε
case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), x ∈ (closedBall 0 (1 / ‖c‖), ε).fst → ↑f x ∈ closedBall 0 (closedBall 0 (1 / ‖c‖), ε).snd
⊢ f ∈ closedBall 0 ε
simp_rw [mem_closedBall_zero_iff] at hf
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
⊢ ‖f‖ ≤ ε
case refine'_1.intro.intro.refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
⊢ f ∈ closedBall 0 ε
convert (@mem_closedBall_zero_iff _ (_) f ε).2 _
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x✝ : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
x : E
hx₁ : 1 / ‖c‖ * ‖c‖ ≤ ‖x‖
hxc : ‖x‖ < 1 / ‖c‖
⊢ ‖↑f x‖ ≤ ε * ‖x‖
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
⊢ ‖f‖ ≤ ε
refine' op_norm_le_of_shell' (div_pos one_pos hc₀) hε.le hc₁ fun x hx₁ hxc => _
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x✝ : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
x : E
hx₁ : 1 ≤ ‖x‖
hxc : ‖x‖ < 1 / ‖c‖
⊢ ‖↑f x‖ ≤ ε * ‖x‖
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x✝ : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
x : E
hx₁ : 1 / ‖c‖ * ‖c‖ ≤ ‖x‖
hxc : ‖x‖ < 1 / ‖c‖
⊢ ‖↑f x‖ ≤ ε * ‖x‖
rw [div_mul_cancel 1 hc₀.ne.symm] at hx₁
no goals
case refine'_1.intro.intro.refine'_2.convert_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f✝ g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x✝ : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
f : E →SL[σ₁₂] F
hf : ∀ (x : E), ‖x‖ ≤ 1 / ‖c‖ → ‖↑f x‖ ≤ ε
x : E
hx₁ : 1 ≤ ‖x‖
hxc : ‖x‖ < 1 / ‖c‖
⊢ ‖↑f x‖ ≤ ε * ‖x‖
exact (hf x hxc.le).trans (le_mul_of_one_le_right hε.le hx₁)
no goals
case refine'_1.intro.intro.refine'_1
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
c : 𝕜
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
ε : ℝ
hε : 0 < ε
⊢ Bornology.IsVonNBounded 𝕜 (closedBall 0 (1 / ‖c‖), ε).fst
exact NormedSpace.isVonNBounded_closedBall _ _ _
case refine'_2.mk.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Bornology.IsVonNBounded 𝕜 (S, ε).fst
hε : 0 < (S, ε).snd
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
case refine'_2
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
⊢ ∀ (i' : Set E × ℝ),
    Bornology.IsVonNBounded 𝕜 i'.fst ∧ 0 < i'.snd →
      ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ i'.fst → ↑f x ∈ closedBall 0 i'.snd}
rintro ⟨S, ε⟩ ⟨hS, hε⟩
case refine'_2.mk.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Metric.Bounded (S, ε).fst
hε : 0 < (S, ε).snd
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
case refine'_2.mk.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Bornology.IsVonNBounded 𝕜 (S, ε).fst
hε : 0 < (S, ε).snd
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
rw [NormedSpace.isVonNBounded_iff, ← bounded_iff_isBounded] at hS
case refine'_2.mk.intro.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Metric.Bounded (S, ε).fst
hε : 0 < (S, ε).snd
δ : ℝ
hδ : 0 < δ
hSδ : (S, ε).fst ⊆ closedBall 0 δ
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
case refine'_2.mk.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Metric.Bounded (S, ε).fst
hε : 0 < (S, ε).snd
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
rcases hS.subset_ball_lt 0 0 with ⟨δ, hδ, hSδ⟩
no goals
case refine'_2.mk.intro.intro.intro
𝕜 : Type u_3
𝕜₂ : Type u_4
𝕜₃ : Type ?u.560425
E : Type u_1
Eₗ : Type ?u.560431
F : Type u_2
Fₗ : Type ?u.560437
G : Type ?u.560440
Gₗ : Type ?u.560443
𝓕 : Type ?u.560446
inst✝¹⁷ : SeminormedAddCommGroup E
inst✝¹⁶ : SeminormedAddCommGroup Eₗ
inst✝¹⁵ : SeminormedAddCommGroup F
inst✝¹⁴ : SeminormedAddCommGroup Fₗ
inst✝¹³ : SeminormedAddCommGroup G
inst✝¹² : SeminormedAddCommGroup Gₗ
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜₂
inst✝⁹ : NontriviallyNormedField 𝕜₃
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace 𝕜 Eₗ
inst✝⁶ : NormedSpace 𝕜₂ F
inst✝⁵ : NormedSpace 𝕜 Fₗ
inst✝⁴ : NormedSpace 𝕜₃ G
inst✝³ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomIsometric σ₁₂
inst✝ : RingHomIsometric σ₂₃
f g : E →SL[σ₁₂] F
h : F →SL[σ₂₃] G
x : E
S : Set E
ε : ℝ
hS : Metric.Bounded (S, ε).fst
hε : 0 < (S, ε).snd
δ : ℝ
hδ : 0 < δ
hSδ : (S, ε).fst ⊆ closedBall 0 δ
⊢ ∃ i, 0 < i ∧ closedBall 0 i ⊆ {f | ∀ (x : E), x ∈ (S, ε).fst → ↑f x ∈ closedBall 0 (S, ε).snd}
exact ⟨ε / δ, div_pos hε hδ,
  (ContinuousLinearMap.tmp_closedBall_div_subset hε hδ).trans fun f hf x hx => hf x <| hSδ hx⟩