dual_flip_dual_dual_flip — Mathlib

English

The dual of a union equals the infimum (intersection) of duals of the members.

Русский

Двойственный конус объединения равен частному пересечению двойственных конусов членов.

LaTeX

$$$\\operatorname{dual} p(\\bigcup\\_i f(i)) = \\bigcap\i \\operatorname{dual} p(f(i))$$$

Lean4

@[simp]
theorem dual_flip_dual_dual_flip (s : Set N) : dual p.flip (dual p (dual p.flip s)) = dual p.flip s :=
  dual_dual_flip_dual _

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