krullDim_le_of_krullDim_preimage_le'

English

If f: α → β is a monotone map and ∀ x ∈ β, krullDim(f⁻¹({x})) ≤ m, then krullDim(α) ≤ (m+1)·krullDim(β) + m.

Русский

Если f: α → β монотоном и для всех x ∈ β krullDim(f⁻¹({x})) ≤ m, то krullDim(α) ≤ (m+1)·krullDim(β) + m.

LaTeX

$$$\\forall f:\\alpha \\to \\beta,\\; \\text{Monotone}(f) \\land (\\forall x,\\operatorname{krullDim}(f^{-1}\\{x\\}) \\le m) \\Rightarrow \\operatorname{krullDim}(\\alpha) \\le (m+1)\\operatorname{krullDim}(\\beta) + m$.$$

Lean4

/-- Another version when the `OrderHom` is unbundled -/
theorem krullDim_le_of_krullDim_preimage_le' (f : α → β) (h_mono : Monotone f)
    (h : ∀ (x : β), Order.krullDim (f ⁻¹' { x }) ≤ m) : Order.krullDim α ≤ (m + 1) * Order.krullDim β + m :=
  Order.krullDim_le_of_krullDim_preimage_le ⟨f, h_mono⟩ h

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