convex_hyperplane — Mathlib

English

The set {w ∈ E | f(w) = r} is convex for a linear map f and scalar r; it is the intersection of the ≤ and ≥ half-spaces.

Русский

Гиперплоскость {w : f(w) = r} выпукла; она является пересечением полупространств ≤ и ≥.

LaTeX

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

Lean4

theorem convex_hyperplane {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 {w | f w = r} :=
  by
  simp_rw [le_antisymm_iff]
  exact (convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

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