innerDual_sUnion — Mathlib

English

The dual of the set-theoretic union over a family S equals the infimum over the duals of elements of S.

Русский

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

LaTeX

$$$\\text{innerDual}(\\bigcup S)=\\bigwedge_{s\\in S} innerDual(s)$$$

Lean4

theorem innerDual_sUnion (S : Set (Set E)) : innerDual (⋃₀ S) = sInf (innerDual '' S) := by ext;
  simp [forall_swap (α := E)]

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