polar_eq_iInter — Mathlib

English

The polar of s equals the intersection over x ∈ s of the corresponding sets {y ∈ F : ‖B x y‖ ≤ 1}.

Русский

Поляр множества s равна пересечению по x ∈ s множества {y ∈ F : ‖B x y‖ ≤ 1}.

LaTeX

$$$B.polar(s) = \bigcap_{x \in s} \{ y \in F : \|B(x,y)\| \le 1 \}$$$

Lean4

theorem polar_eq_iInter {s : Set E} : B.polar s = ⋂ x ∈ s, {y : F | ‖B x y‖ ≤ 1} :=
  by
  ext
  simp only [polar_mem_iff, Set.mem_iInter, Set.mem_setOf_eq]

Похожие утверждения