convex_ge — Mathlib

English

If a function f is monotone on a convex set s, then the set {x ∈ s | f(x) ≤ r} is convex for any r.

Русский

Если функция монотонна на выпуклом множества, то множество {x ∈ s | f(x) ≤ r} выпукло.

LaTeX

$$$\operatorname{Convex}_\mathbb{K}(\{x \in s : f(x) \le r\})$ under appropriate monotonicity conditions$$

Lean4

theorem convex_ge (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | r ≤ f x}) :=
  MonotoneOn.convex_le (E := Eᵒᵈ) (β := βᵒᵈ) hf.dual hs r

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