Theorems · Theorem · order theory

Order.height_strictMono

∀ {α : Type u_1} [inst : Preorder α] {x y : α}, x < y → Order.height x < ⊤ → Order.height x < Order.height y

For elements of finite height, height is strictly monotone.

Defined in

Mathlib.Order.KrullDimension

Cited by

5 results in Mathlib

Foundations

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

Assumes

Preorder