convex — Mathlib

English

For each n, the half-space { x in R^n | x_1 ≥ 0 } is a convex subset of Euclidean space.

Русский

Для каждого n полупространство { x в R^n | x_1 ≥ 0 } является выпуклым подмножеством Евклидова пространства.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\mathrm{Convex}_{\\mathbb{R}}\\{ x \\in \\mathbb{R}^{\\mathrm{Fin}(n)} \\mid x_1 \\ge 0 \\}$$$

Lean4

theorem convex [NeZero n] : Convex ℝ {x : EuclideanSpace ℝ (Fin n) | 0 ≤ x 0} := fun _ hx _ hy _ _ _ _ _ ↦ by
  dsimp at hx hy ⊢; positivity

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