nullHomotopicMap'_f_eq_zero — Mathlib

English

Similarly, if the indexing relations eliminate all possible j i pairs for the subscript, then the f-component of the null-homotopic map constructed with h is the zero morphism.

Русский

Аналогично, если перестановка индексов исключает все отношения j i, то f-компонента нулевой гомотопической карты, построенной с помощью h, равна нулю.

LaTeX

$$$ (\mathrm{nullHomotopicMap'} h).f_{k_0} = 0 $$$

Lean4

@[simp]
theorem nullHomotopicMap'_f_eq_zero {k₀ : ι} (hk₀ : ∀ l : ι, ¬c.Rel k₀ l) (hk₀' : ∀ l : ι, ¬c.Rel l k₀)
    (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) : (nullHomotopicMap' h).f k₀ = 0 :=
  by
  simp only [nullHomotopicMap']
  apply nullHomotopicMap_f_eq_zero hk₀ hk₀'

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