gc_hull_coe — Mathlib

English

The hull operator hull_R: Set M → ConvexCone R M is left adjoint to the inclusion map ↑ : ConvexCone R M → Set M. Equivalently, for all s ⊆ M and C ∈ ConvexCone R M, hull_R(s) ≤ C iff s ⊆ C.

Русский

Оператор оболочки hull_R: Set M → ConvexCone R M является левым сопряжением вложения ConvexCone в множества. Эквивалентно: для любых s ⊆ M и C ∈ ConvexCone R M верна эквивалентность hull_R(s) ≤ C ⇔ s ⊆ C.

LaTeX

$$$\forall s \subseteq M, \forall C \in \text{ConvexCone } R\, M:\, \operatorname{hull}_R(s) \le C \iff s \subseteq C$$$

Lean4

theorem gc_hull_coe : GaloisConnection (hull R : Set M → ConvexCone R M) (↑) := fun _C _s ↦ hull_le_iff

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