𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
have Rpos : 0 < R := (norm_nonneg _).trans_lt hR
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
have : ‖c‖ / R < 1 := by
  rw [div_lt_iff Rpos]
  simpa using hR
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
have x0 : x ≠ 0 := fun H => by simp [H] at xF
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
obtain ⟨d, d0, dxlt, ledx, -⟩ :
  ∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < R ∧ R / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ R⁻¹ * ‖c‖ * ‖x‖ :=
  rescale_to_shell hc Rpos x0
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖d • x - y‖
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
refine' ⟨d • x, dxlt.le, fun y hy => _⟩
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ 1 ≤ ‖d • x - y‖
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖d • x - y‖
set y' := d⁻¹ • y
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 ≤ ‖d • x - y‖
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ 1 ≤ ‖d • x - y‖
have yy' : y = d • y' := by simp [smul_smul, mul_inv_cancel d0]
no goals
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 ≤ ‖d • x - y‖
calc
  1 = ‖c‖ / R * (R / ‖c‖) := by field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
  _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
  _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
    simp [norm_smul]
    ring
  _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [Submodule.smul_mem _ _ hy])
  _ = ‖d • x - y‖ := by rw [yy', ←smul_sub, norm_smul]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ‖c‖ < 1 * R
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ‖c‖ / R < 1
rw [div_lt_iff Rpos]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ‖c‖ < 1 * R
simpa using hR
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
H : x = 0
⊢ False
simp [H] at xF
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ y = d • y'
simp [smul_smul, mul_inv_cancel d0]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 = ‖c‖ / R * (R / ‖c‖)
field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
gcongr
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (‖d‖ * ‖x‖) = ‖d‖ * (‖c‖ / R * ‖x‖)
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
simp [norm_smul]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (‖d‖ * ‖x‖) = ‖d‖ * (‖c‖ / R * ‖x‖)
ring
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖x‖ ≤ ‖x - y'‖
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖
gcongr
no goals
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖x‖ ≤ ‖x - y'‖
exact hx y' (by simp [Submodule.smul_mem _ _ hy])
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ y' ∈ F
simp [Submodule.smul_mem _ _ hy]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.15017
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
rw [yy', ←smul_sub, norm_smul]