HomotopyRel — Mathlib

English

A HomotopyRel f0 f1 S is a homotopy between f0 and f1 that is fixed on S.

Русский

Гомотопия между f0 и f1 фиксирована на S.

LaTeX

$$HomotopyRel f0 f1 S := HomotopyWith f0 f1 (λ f, ∀ x ∈ S, f x = f0 x)$$

Lean4

/-- A `HomotopyRel f₀ f₁ S` is a homotopy between `f₀` and `f₁` which is fixed on the points in `S`.
-/
abbrev HomotopyRel (f₀ f₁ : C(X, Y)) (S : Set X) :=
  HomotopyWith f₀ f₁ fun f ↦ ∀ x ∈ S, f x = f₀ x

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