disjoint_hull_right_of_convex — Mathlib

English

The symmetric statement to hull-left disjointness: for a convex 𝕜-set s and a convex cone C, Disjoint C (hull 𝕜 s) is equivalent to Disjoint (carrier of C) s.

Русский

Симметричная формулировка раздельности: Disjoint C (hull 𝕜 s) эквивалентно Disjoint (носитель C) s.

LaTeX

$$$Disjoint\\,C\\,(\\mathrm{hull}_{\\mathbb{K}}(s)) \\iff \\mathrm{Disjoint}(|C|, s)$$$

Lean4

theorem disjoint_hull_right_of_convex (hs : Convex 𝕜 s) : Disjoint C (hull 𝕜 s) ↔ Disjoint (↑C) s := by
  rw [disjoint_comm, disjoint_hull_left_of_convex hs, disjoint_comm]

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