convex_lt — Mathlib

English

For every real r, the sublevel set {x in s | f(x) < r} is convex.

Русский

Для каждого числа r, множество {x ∈ s | f(x) < r} выпукло.

LaTeX

$$$\forall r\in\mathbb{R},\; \{x\in s \mid f(x)

Lean4

theorem convex_lt (hf : StrictConvexOn 𝕜 s f) (r : β) : Convex 𝕜 ({x ∈ s | f x < r}) :=
  convex_iff_pairwise_pos.2 fun x hx y hy hxy a b ha hb hab =>
    ⟨hf.1 hx.1 hy.1 ha.le hb.le hab,
      calc
        f (a • x + b • y) < a • f x + b • f y := hf.2 hx.1 hy.1 hxy ha hb hab
        _ ≤ a • r + b • r := by
          gcongr
          · exact hx.2.le
          · exact hy.2.le
        _ = r := Convex.combo_self hab r⟩

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