isSupportedOutside₁_iff — Mathlib

English

For any complex K, K is supported outside e1 if and only if K is supported outside e2.

Русский

Для любого комплекса K: K поддержан вне e1 тогда и только тогда, когда он поддержан вне e2.

LaTeX

$$$K.IsSupportedOutside\ e_1 \iff K.IsSupportedOutside\ e_2.$$$

Lean4

theorem isSupportedOutside₁_iff : K.IsSupportedOutside e₁ ↔ K.IsSupported e₂ :=
  by
  constructor
  · intro h
    exact
      ⟨fun i hi => by
        obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
        exact h.exactAt i₁⟩
  · intro _
    exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _ (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

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