innerDualCone_univ — Mathlib

English

Dual of a union over an index set equals the infimum of duals.

Русский

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

LaTeX

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

Lean4

/-- Dual cone of the total space is the convex cone {0}. -/
@[deprecated ProperCone.innerDual_univ (since := "2025-07-06")]
theorem innerDualCone_univ : (univ : Set H).innerDualCone = 0 :=
  by
  suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0
    by
    apply SetLike.coe_injective
    exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩
  exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)

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