English
The dual cone with respect to p does not change when replacing a generating set by its span. In symbols, dual_p(span_R(s)) = dual_p(s).
Русский
Двойственный конус относительно p не изменяется, если подмножество заменено на его порождающее множество, содержащее все линейные комбинации его элементов; то есть dual_p(span_R(s)) = dual_p(s).
LaTeX
$$$\mathrm{dual}_{p}(\operatorname{span}_{R}(s)) = \mathrm{dual}_{p}(s)$$$
Lean4
@[simp]
theorem dual_span (s : Set M) : dual p (span R s) = dual p s :=
by
refine le_antisymm (dual_le_dual Submodule.subset_span) (fun x hx y hy => ?_)
induction hy using Submodule.span_induction with
| mem _y h => exact hx h
| zero => simp
| add y z _hy _hz hy hz => rw [map_add, add_apply]; exact add_nonneg hy hz
| smul t y _hy hy => rw [map_smul_of_tower, Nonneg.mk_smul, smul_apply]; exact mul_nonneg t.2 hy
