English
Two constant maps from Y to X are homotopic if and only if their target points are joined by a path in Y (assuming Y is nonempty).
Русский
Две константные отображения из Y в X гомотопичны тогда и только тогда, когда их значения в Y соединяются путём в Y (при условии, что Y не пуст).
LaTeX
$$$(\mathrm{ContinuousMap.const}\; Y\; x_0)\;\mathrm{Homotopic}\; (\mathrm{ContinuousMap.const}\; Y\; x_1) \;\Longleftrightarrow\; \mathrm{Joined}\; x_0 x_1$$$
Lean4
/-- Two constant continuous maps with nonempty domain are homotopic if and only if their values are
joined by a path in the codomain. -/
@[simp]
theorem homotopic_const_iff [Nonempty Y] :
(ContinuousMap.const Y x₀).Homotopic (ContinuousMap.const Y x₁) ↔ Joined x₀ x₁ :=
by
inhabit Y
refine ⟨fun ⟨H⟩ ↦ ⟨⟨(H.toContinuousMap.comp .prodSwap).curry default, ?_, ?_⟩⟩, fun ⟨p⟩ ↦ ⟨p.toHomotopyConst⟩⟩ <;>
simp
