mono — Mathlib

English

If n ≤ m and α satisfies KrullDimLE n α, then α also satisfies KrullDimLE m.

Русский

Если n ≤ m и выполняется свойство KrullDimLE n α, то оно верно и для m.

LaTeX

$$$n \le m \Rightarrow (\operatorname{KrullDimLE}\ n\ α) \Rightarrow (\operatorname{KrullDimLE}\ m\ α)$$$

Lean4

theorem mono {n m : ℕ} (e : n ≤ m) (α : Type*) [Preorder α] [KrullDimLE n α] : KrullDimLE m α :=
  ⟨KrullDimLE.krullDim_le (n := n).trans (Nat.cast_le.mpr e)⟩

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