Theorems · Theorem · order theory

Order.krullDim_le_of_krullDim_preimage_le

∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] {m : ℕ} (f : α →o β),
  (∀ (x : β), Order.krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m) → Order.krullDim α ≤ (↑m + 1) * Order.krullDim β + ↑m

Defined in

Mathlib.Order.KrullDimension

Cited by

1 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderPartialOrder