innerDualCone_le_innerDualCone — Mathlib

English

Relative hyperplane separation results imply monotonicity with respect to set inclusion for inner dual cones.

Русский

Результаты разделения гиперплоскостью дают монотонность двойных конусов по включению множеств.

LaTeX

$$$t\\subseteq s\\Rightarrow innerDual(s)\\le innerDual(t)$$$

Lean4

@[deprecated ProperCone.innerDual_le_innerDual (since := "2025-07-06")]
theorem innerDualCone_le_innerDualCone (h : t ⊆ s) : s.innerDualCone ≤ t.innerDualCone := fun _ hy x hx => hy x (h hx)

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