convex_le — Mathlib

English

Let f be a monotone function from E to β. For every real r, the sublevel set {x ∈ E | f(x) ≤ r} is convex (with respect to 𝕜).

Русский

Пусть f: E → β монотонна. Для любого b-равного значения r множество уровня {x ∈ E | f(x) ≤ r} выпукло по отношению к 𝕜.

LaTeX

$$$$ \\forall f : E \\to \\beta,\\ \\operatorname{Monotone} f \\rightarrow \\forall r,\\ \\operatorname{Convex}_{\\mathbb{K}}(\\{x \\in E \\mid f(x) \\le r\\}). $$$$

Lean4

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

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