isZero_stupidTrunc_iff — Mathlib

English

The truncated complex K.stupidTrunc(e) is zero if and only if K is strictly supported outside e.

Русский

Усечение K.stupidTrunc(e) равно нулю тогда и только тогда, когда K строго поддержано вне e.

LaTeX

$$$IsZero\bigl(K.\mathrm{stupidTrunc}(e)\bigr)\ \iff\ K.\mathrm{IsStrictlySupportedOutside}(e)$$$

Lean4

theorem isZero_stupidTrunc_iff : IsZero (K.stupidTrunc e) ↔ K.IsStrictlySupportedOutside e :=
  by
  constructor
  · exact fun h ↦ ⟨fun i ↦ ((eval _ _ (e.f i)).map_isZero h).of_iso (K.stupidTruncXIso e rfl).symm⟩
  · intro h
    rw [isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside _ e]
    constructor
    · infer_instance
    · exact ⟨fun i ↦ (h.isZero i).of_iso (K.stupidTruncXIso e rfl)⟩

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