Theorems · Inductive type · order theory

Order.IsNormal

{α : Type u_1} → {β : Type u_2} → [LinearOrder α] → [LinearOrder β] → (α → β) → Prop

A normal function between well-orders is a strictly monotonic continuous function.

Defined in

Mathlib.Order.IsNormal

Cited by

118 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

LinearOrderLinearOrder