convex_gt — Mathlib

English

Let f be monotone. For every r ∈ β, the sublevel set {x ∈ E : f(x) ≤ r} is convex.

Русский

Пусть f монотонна. Для любого r ∈ β множество {x ∈ E : f(x) ≤ r} выпукло.

LaTeX

$$$$ \\operatorname{Convex}_{\\mathbb{K}}\\bigl\\{ x \\in E \\mid f(x) \\le r \\bigr\\} $$$$

Lean4

theorem convex_gt (hf : Monotone f) (r : β) : Convex 𝕜 {x | f x ≤ r} :=
  Set.sep_univ.subst ((hf.monotoneOn univ).convex_le convex_univ r)

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