dual_le_dual — Mathlib

English

The dual cone of a union is the intersection of dual cones: dual p (s ∪ t) = dual p s ∩ dual p t.

Русский

Двойственный конус объединения равен пересечению двойственных конусов: dual p(s ∪ t) = dual p s ⊓ dual p t.

LaTeX

$$$\\operatorname{dual} p (s \\cup t) = \\operatorname{dual} p s \\cap \\operatorname{dual} p t$$$

Lean4

@[gcongr]
theorem dual_le_dual (h : t ⊆ s) : dual p s ≤ dual p t := fun _y hy _x hx ↦ hy (h hx)

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