contractibleSpace — Mathlib

English

A nonempty convex set is contractible: there exists a deformation retract to a point inside the set.

Русский

Не пустое выпуклое множество контрактно: существует деформирующее отображение к точке внутри множества.

LaTeX

$$$$\\text{Convex}(\\mathbb{R}, s) \\land s \\neq \\varnothing \\Rightarrow \\text{ContractibleSpace}(s).$$$$

Lean4

/-- A non-empty convex set is a contractible space. -/
protected theorem contractibleSpace (hs : Convex ℝ s) (hne : s.Nonempty) : ContractibleSpace s :=
  let ⟨_, hx⟩ := hne
  (hs.starConvex hx).contractibleSpace hne

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