isStrictlySupportedOutside₁_iff

English

For a fixed pair of complementary embeddings, and a complex K, K is strictly supported outside e1 if and only if it is strictly supported outside e2.

Русский

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

LaTeX

$$$K\ IsStrictlySupportedOutside\ e_1 \iff K\ IsStrictlySupportedOutside\ e_2.$$$

Lean4

theorem isStrictlySupportedOutside₁_iff : K.IsStrictlySupportedOutside e₁ ↔ K.IsStrictlySupported e₂ :=
  by
  constructor
  · intro h
    exact
      ⟨fun i hi => by
        obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
        exact h.isZero i₁⟩
  · intro _
    exact ⟨fun i₁ => K.isZero_X_of_isStrictlySupported e₂ _ (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

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