English
Any nonempty star-convex set is contractible: there exists a continuous deformation retract to a point within the set.
Русский
Любое непустое звездообразное множество контрактивно: существует непрерывное деформирующее отображение, переводящее множество в точку внутри множества.
LaTeX
$$$$\\text{StarConvex}(\\mathbb{R}, x, s) \\land s \\neq \\emptyset \\;\Rightarrow\\; \\text{ContractibleSpace}(s).$$$$
Lean4
/-- A non-empty star convex set is a contractible space. -/
protected theorem contractibleSpace (h : StarConvex ℝ x s) (hne : s.Nonempty) : ContractibleSpace s :=
by
refine
(contractible_iff_id_nullhomotopic s).2
⟨⟨x, h.mem hne⟩, ⟨⟨⟨fun p => ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x => ?_, fun x => ?_⟩⟩⟩
· exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)
·
exact
((continuous_subtype_val.fst'.smul continuous_const).add
((continuous_const.sub continuous_subtype_val.fst').smul continuous_subtype_val.snd')).subtype_mk
_
· simp
· simp
