refl — Mathlib

English

If f is fixed to satisfy P, there is a trivial homotopy from f to f preserving P.

Русский

Если f удовлетворяет P, существует тривиальная гомотопия от f к f, сохраняющая P.

LaTeX

$$$\\exists H : HomotopyWith(f,f,P),\\; H = \\text{refl}(f, hf)$$$

Lean4

/-- Given a continuous function `f`, and a proof `h : P f`, we can define a `HomotopyWith f f P` by
`F (t, x) = f x`
-/
@[simps!]
def refl (f : C(X, Y)) (hf : P f) : HomotopyWith f f P
    where
  toHomotopy := Homotopy.refl f
  prop' := fun _ => hf

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