dual_insert — Mathlib

English

An existential extension q dominating p exists with domain ⊤ and preserving nonnegativity on a cone s.

Русский

Существует расширение q, превосходящее p, домен которого совпадает с верхней границей, и сохраняет неотрицательность на s.

LaTeX

$$∃ q ≥ p, q.domain = ⊤ ∧ ∀ x : q.domain, x ∈ s → 0 ≤ q x$$

Lean4

theorem dual_insert (x : M) (s : Set M) : dual p (insert x s) = dual p { x } ⊓ dual p s := by rw [insert_eq, dual_union]

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