dual_univ — Mathlib

English

The dual cone of the universal set is the zero subspace: dual p univ = 0.

Русский

Двойственный конус полного множества равен нулевому подпространству: dual p univ = 0.

LaTeX

$$$\\operatorname{dual} p\\, \\mathrm{univ} = 0$$$

Lean4

theorem dual_univ (hp : Injective p.flip) : dual p univ = 0 :=
  by
  refine le_antisymm (fun y hy ↦ (_root_.map_eq_zero_iff p.flip hp).1 ?_) (by simp)
  ext x
  exact (hy <| mem_univ x).antisymm' <| by simpa using hy <| mem_univ (-x)

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