cast — Mathlib

English

If f0 = g0 and f1 = g1, then a Homotopy F between f0 and f1 yields a Homotopy between g0 and g1 by transporting along the equalities.

Русский

Если f0 = g0 и f1 = g1, то гомотопия F между f0 и f1 переходит в гомотопию между g0 и g1 по переносу вдоль равенств.

LaTeX

$$$$ F : \mathrm{Homotopy}(f_0, f_1), \ h_0: f_0 = g_0, \ h_1: f_1 = g_1 \;\Rightarrow\; \mathrm{Homotopy}(g_0, g_1) $$$$

Lean4

/-- Casting a `Homotopy f₀ f₁` to a `Homotopy g₀ g₁` where `f₀ = g₀` and `f₁ = g₁`.
-/
@[simps]
def cast {f₀ f₁ g₀ g₁ : C(X, Y)} (F : Homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : Homotopy g₀ g₁
    where
  toFun := F
  map_zero_left := by simp [← h₀]
  map_one_left := by simp [← h₁]

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