HomotopicRel — Mathlib

English

ContinuousMap.HomotopicRel f0 f1 S denotes that f0 and f1 are homotopic relative to a set S; i.e., there exists a HomotopyRel f0 f1 S.

Русский

ContinuousMap.HomotopicRel f0 f1 S означает, что f0 и f1 гомотопичны относительно множества S; то есть существует HomotopyRel f0 f1 S.

LaTeX

$$Definitional: HomotopicRel(f0, f1, S) := Nonempty (HomotopyRel f0 f1 S).$$

Lean4

/-- Given continuous maps `f₀` and `f₁`, we say `f₀` and `f₁` are homotopic relative to a set `S` if
there exists a `HomotopyRel f₀ f₁ S`.
-/
def HomotopicRel (f₀ f₁ : C(X, Y)) (S : Set X) : Prop :=
  Nonempty (HomotopyRel f₀ f₁ S)

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