ampleSet_univ — Mathlib

English

The entire space is ample: in a normed real vector space, the set consisting of all points is ample.

Русский

Векторное пространство в целом является ампельным: множество всех точек пространства ампельно.

LaTeX

$$$\mathrm{AmpleSet}(\mathrm{univ})$$$

Lean4

/-- A whole vector space is ample. -/
@[simp]
theorem ampleSet_univ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : AmpleSet (univ : Set F) :=
  by
  intro x _
  rw [connectedComponentIn_univ, PreconnectedSpace.connectedComponent_eq_univ, convexHull_univ]

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