starConvex_compl_Iic — Mathlib

English

If x<y, then the complement of (−∞,x] is star-convex at y.

Русский

Если x меньше y, то дополнение множества (-∞,x] звёздочно выпукло относительно y.

LaTeX

$$$\\text{starConvex}_{\\mathbb{K}}(y, (-\\infty,x]^{c})$ при $x

Lean4

/-- If `x < y`, then `(Set.Iic x)ᶜ` is star convex at `y`. -/
theorem starConvex_compl_Iic (h : x < y) : StarConvex 𝕜 y (Iic x)ᶜ :=
  by
  refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_
  rw [mem_compl_iff, mem_Iic] at hz ⊢
  contrapose! hz
  refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le
  calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

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