Theorems · Theorem · order theory

Order.height_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) → ∀ (x : α), Order.height x ≤ (↑m + 1) * Order.height (f x) + ↑m

Defined in

Mathlib.Order.KrullDimension

Cited by

2 results in Mathlib

Foundations

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

Assumes

PreorderPartialOrder