convex — Mathlib

English

If f is antitone, then for every r the set {x ∈ E : r < f(x)} is convex.

Русский

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

LaTeX

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

Lean4

/-- Affine subspaces are convex. -/
theorem convex (Q : AffineSubspace 𝕜 E) : Convex 𝕜 (Q : Set E) := fun x hx y hy a b _ _ hab ↦ by
  simpa [Convex.combo_eq_smul_sub_add hab] using Q.2 _ hy hx hx

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