English
Two maps f0,f1: A→E are homotopic rel S if and only if their compositions with p are homotopic rel S, provided there exists a point in S where they agree.
Русский
Два отображения f0,f1: A→E гомотопны относительно S тогда и только тогда, когда их композиции с p гомотопны относительно S, при условии, что существует точка в S, в которой они совпадают.
LaTeX
$$$$f_0.HomotopicRel f_1 S \iff (p\circ f_0)\,\text{HomotopicRel}\,(p\circ f_1)\;S,$$$$
Lean4
/-- Two continuous maps from a preconnected space to the total space of a covering map
are homotopic relative to a set `S` if and only if their compositions with the covering map
are homotopic relative to `S`, assuming that they agree at a point in `S`. -/
theorem homotopicRel_iff_comp [PreconnectedSpace A] {f₀ f₁ : C(A, E)} {S : Set A} (he : ∃ a ∈ S, f₀ a = f₁ a) :
f₀.HomotopicRel f₁ S ↔ (ContinuousMap.comp ⟨p, cov.continuous⟩ f₀).HomotopicRel (.comp ⟨p, cov.continuous⟩ f₁) S :=
⟨fun ⟨F⟩ ↦ ⟨F.compContinuousMap _⟩, fun ⟨F⟩ ↦ ⟨cov.liftHomotopyRel F he rfl rfl⟩⟩
