disjoint_hull_left_of_convex — Mathlib

English

For a convex 𝕜-set s and a convex cone C, the hull of s is disjoint from C if and only if s is disjoint from the carrier of C.

Русский

Для выпуклого множества s и конуса C вершины оболочки hull 𝕜 s и C не пересекаются тогда и только тогда, когда множество s не пересекается с носителем конуса C.

LaTeX

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

Lean4

theorem disjoint_hull_left_of_convex (hs : Convex 𝕜 s) : Disjoint (hull 𝕜 s) C ↔ Disjoint s C
    where
  mp := by rw [← disjoint_coe]; exact .mono_left subset_hull
  mpr := by
    simp_rw [← disjoint_coe, disjoint_left, SetLike.mem_coe, mem_hull_of_convex hs]
    rintro hsC _ ⟨r, hr, y, hy, rfl⟩
    exact (C.smul_mem_iff hr).not.mpr (hsC hy)

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