convex_lt — Mathlib

English

The hyperplane {w | f(w) = r} is convex, as the intersection of two convex half-spaces.

Русский

Гиперплоскость {w : f(w)=r} выпукла, как пересечение выпуклых полупространств.

LaTeX

$$$\{x \in E : f(x)=r\}$ выпукло$$

Lean4

theorem convex_lt (hf : MonotoneOn f s) (hs : Convex 𝕜 s) (r : β) : Convex 𝕜 ({x ∈ s | f x < r}) :=
  fun x hx y hy _ _ ha hb hab =>
  ⟨hs hx.1 hy.1 ha hb hab,
    (hf (hs hx.1 hy.1 ha hb hab) (max_rec' s hx.1 hy.1) (Convex.combo_le_max x y ha hb hab)).trans_lt
      (max_rec' {x | f x < r} hx.2 hy.2)⟩

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