Theorems · Theorem · order theory

Order.isNormal_iff

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f ↔ StrictMono f ∧ ∀ (o : α), Order.IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a

Defined in

Mathlib.Order.IsNormal

Cited by

8 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Quot.sound

Assumes

LinearOrderLinearOrder