convex — Mathlib

English

Let Q_n = { x ∈ R^n | x_i ≥ 0 for all i }. Then Q_n is a convex subset of R^n.

Русский

Пусть Q_n = { x ∈ R^n | все координаты неотрицательны }. Тогда Q_n выпуклое подмножество R^n.

LaTeX

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

Lean4

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

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