hull_le_iff — Mathlib

English

Let R be a semiring with a partial order acting on an additive commutative monoid M. For any convex cone C in M and any subset s of M, the hull of s with respect to R is contained in C if and only if s is contained in C.

Русский

Пусть R — полукольцо с частично упорядочением, действующее на добавочно-коммутативный моноид M. Для любого выпуклого конуса C in M и любого подмножества s⊆M оболочка hull_R(s) содержится в C тогда и только если s⊆C.

LaTeX

$$$\operatorname{hull}_R(s) \le C \iff s \subseteq C$$$

Lean4

theorem hull_le_iff : hull R s ≤ C ↔ s ⊆ C :=
  ⟨subset_hull.trans, hull_min⟩

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