polar_gc — Mathlib

English

Polar commutes with unions: polar of the union equals the intersection of polars.

Русский

Поляризация сохраняет объединения: поляр объединения равна пересечению поляр.

LaTeX

$$$B.polar(\bigcup i\, s_i) = \bigcap i, B.polar(s_i)$$$

Lean4

/-- The map `B.polar : Set E → Set F` forms an order-reversing Galois connection with
`B.flip.polar : Set F → Set E`. We use `OrderDual.toDual` and `OrderDual.ofDual` to express
that `polar` is order-reversing. -/
theorem polar_gc : GaloisConnection (OrderDual.toDual ∘ B.polar) (B.flip.polar ∘ OrderDual.ofDual) := fun _ _ =>
  ⟨fun h _ hx _ hy => h hy _ hx, fun h _ hx _ hy => h hy _ hx⟩

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