case h
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ polar B s ↔ x✝ ∈ ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ polar B s = ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
ext
no goals
case h
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝ : F
⊢ x✝ ∈ polar B s ↔ x✝ ∈ ⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑B x) y‖ ≤ 1}
simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]