𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ ∧ ∀ (x : F), x ∈ polar B Set.univ → x = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ polar B Set.univ = {0}
rw [Set.eq_singleton_iff_unique_mem]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
⊢ ↑(↑B x) y = 0
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ ∧ ∀ (x : F), x ∈ polar B Set.univ → x = 0
refine' ⟨by simp only [zero_mem_polar], fun y hy => h _ fun x => _⟩
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
⊢ ↑(↑B x) y = 0
refine' norm_le_zero_iff.mp (le_of_forall_le_of_dense fun ε hε => _)
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
rcases NormedField.exists_norm_lt 𝕜 hε with ⟨c, hc, hcε⟩
no goals
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ ≤ ε
calc
  ‖B x y‖ = ‖c‖ * ‖B (c⁻¹ • x) y‖ := by
    rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv,
      mul_inv_cancel_left₀ hc.ne']
  _ ≤ ε * 1 := by gcongr; exact hy _ trivial
  _ = ε := mul_one _
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
⊢ 0 ∈ polar B Set.univ
simp only [zero_mem_polar]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B x) y‖ = ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖
rw [B.map_smul, LinearMap.smul_apply, Algebra.id.smul_eq_mul, norm_mul, norm_inv,
  mul_inv_cancel_left₀ hc.ne']
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B (c⁻¹ • x)) y‖ ≤ 1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖c‖ * ‖↑(↑B (c⁻¹ • x)) y‖ ≤ ε * 1
gcongr
no goals
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
h : SeparatingRight B
y : F
hy : y ∈ polar B Set.univ
x : E
ε : ℝ
hε : 0 < ε
c : 𝕜
hc : 0 < ‖c‖
hcε : ‖c‖ < ε
⊢ ‖↑(↑B (c⁻¹ • x)) y‖ ≤ 1
exact hy _ trivial