isStrictlyLE_of_iso — Mathlib

English

If K ≅ L and K isStrictlyLE at n, then L isStrictlyLE at n. Linear structure is preserved by isomorphism.

Русский

Если K и L изоморфны и K строго LE в уровне n, то L тоже строго LE в уровне n. Изоморфизм сохраняет свойство LE.

LaTeX

$$$ (K \\cong L) \\Rightarrow (K.IsStrictlyLE(n) \\Rightarrow L.IsStrictlyLE(n)) $$$

Lean4

theorem isStrictlyLE_of_iso (n : ℤ) [K.IsStrictlyLE n] : L.IsStrictlyLE n := by apply isStrictlySupported_of_iso e

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