isZero_X_of_isStrictlySupported — Mathlib

English

If K is strictly supported outside e, then X_i' is zero whenever i' is not in the image of e.

Русский

Если K строго поддержан вне e, то X_i' равен нулю, когда i' не лежит в образе e.

LaTeX

$$$$ \forall i'\; (\forall i, e.f i \neq i') \Rightarrow IsZero(K.X i') $$$$

Lean4

theorem isZero_X_of_isStrictlySupported [K.IsStrictlySupported e] (i' : ι') (hi' : ∀ i, e.f i ≠ i') : IsZero (K.X i') :=
  IsStrictlySupported.isZero i' hi'

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