𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), ↑g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ x = y ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero 𝕜 (x - y)]
no goals
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), ↑g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
simp [sub_eq_zero]