isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside

English

A complex K is zero if and only if it is strictly supported with respect to e and strictly supported outside e.

Русский

Комплекс K равен нулю тогда и только тогда, когда он строго поддержан относительно e и строго поддержан вне e.

LaTeX

$$IsZero(K) \iff (K.IsStrictlySupported(e) \land K.IsStrictlySupportedOutside(e))$$

Lean4

theorem isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside :
    IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e :=
  by
  constructor
  · intro hK
    constructor
    all_goals
      constructor
      intros
      exact (eval _ _ _).map_isZero hK
  · rintro ⟨h₁, h₂⟩
    rw [IsZero.iff_id_eq_zero]
    ext n
    apply IsZero.eq_of_src
    by_cases hn : ∃ i, e.f i = n
    · obtain ⟨i, rfl⟩ := hn
      exact h₂.isZero i
    · exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)

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