innerDual_iUnion — Mathlib

English

The dual of the union over an index set is the infimum (intersection) of the dual cones: innerDual(⋃ i, s_i) = ∧ i, innerDual(s_i).

Русский

Двойной конус объединения по индексу равен пересечению двойных конусов каждого члена: innerDual(⋃i s_i) = ∧i innerDual(s_i).

LaTeX

$$$\\text{innerDual}(\\bigcup_i s_i)=\\bigwedge_i innerDual(s_i)$$$

Lean4

theorem innerDual_iUnion {ι : Sort*} (f : ι → Set E) : innerDual (⋃ i, f i) = ⨅ i, innerDual (f i) := by ext;
  simp [forall_swap (α := E)]

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