isZero_stupidTrunc_X — Mathlib

English

If i' is an index such that no i maps to i' under e.f, then the i'-th component of K.stupidTrunc(e) is zero.

Русский

Если для i' не существует i с e.f i = i', то i'-й компонент K.stupidTrunc(e) равен нулю.

LaTeX

$$$\forall i',\ \big(\forall i, e.f i \neq i'\big)\Rightarrow IsZero\big((K.\mathrm{stupidTrunc}(e)).X(i')\big)$$$

Lean4

theorem isZero_stupidTrunc_X (i' : ι') (hi' : ∀ i, e.f i ≠ i') : IsZero ((K.stupidTrunc e).X i') :=
  isZero_extend_X _ _ _ hi'

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