homotopicRel_empty — Mathlib

English

HomotopicRel f0 f1 ∅ is equivalent to Homotopic f0 f1.

Русский

Гомотопия относительно пустого множества эквивалентна обычной гомотопии.

LaTeX

$$$ HomotopicRel(f_0,f_1,\\emptyset) \\;\\iff\\; Homotopic(f_0,f_1)$$$

Lean4

@[simp]
theorem homotopicRel_empty {f₀ f₁ : C(X, Y)} : HomotopicRel f₀ f₁ ∅ ↔ Homotopic f₀ f₁ :=
  ⟨fun h ↦ h.homotopic, fun ⟨F⟩ ↦ ⟨⟨F, fun _ _ ↦ False.elim⟩⟩⟩

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