sInter_polar_finite_subset_eq_polar

English

A simplified version of the finite-subset polar equality: intersection over a finite family matches the polar.

Русский

Упрощенная версия равенства поляр: пересечение по конечной семье элементов совпадает с поляром.

LaTeX

$$$\bigcap_{i} B.polar(\{s_i\}) = B.polar(\{\,s_i\, : i\})$$$

Lean4

theorem sInter_polar_finite_subset_eq_polar (s : Set E) : ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) = B.polar s :=
  by
  ext x
  simp only [Set.sInter_image, Set.mem_setOf_eq, Set.mem_iInter, and_imp]
  refine ⟨fun hx a ha ↦ ?_, fun hx F _ hF₂ => polar_antitone _ hF₂ hx⟩
  simpa [mem_polar_singleton] using hx _ (Set.finite_singleton a) (Set.singleton_subset_iff.mpr ha)

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