isStrictlySupported_of_iso — Mathlib

English

If K is strictly supported outside e and K ≅ L, then L is strictly supported outside e.

Русский

Если K строго поддержан вне e и K изоморфен L, то L строго поддержан вне e.

LaTeX

$$$$ (K \cong L) \quad \Rightarrow\quad (K \\ IsStrictlySupported e) \Rightarrow (L \\ IsStrictlySupported e) $$$$

Lean4

theorem isStrictlySupported_of_iso [K.IsStrictlySupported e] : L.IsStrictlySupported e where
  isZero i' hi' := (K.isZero_X_of_isStrictlySupported e i' hi').of_iso ((eval _ _ i').mapIso e'.symm)

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