Theorems · Theorem · order theory

strictMonoOn_Iic_of_lt_succ

∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {n : α}, (∀ m < n, ψ m < ψ (Order.succ m)) → StrictMonoOn ψ (Set.Iic n)

A function ψ on a SuccOrder is strictly monotone before some n if for all m such that m < n, we have ψ m < ψ (succ m).

Defined in

Mathlib.Order.Interval.Set.Monotone

Cited by

3 results in Mathlib

Foundations

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

Assumes

PartialOrderPreorderSuccOrderIsSuccArchimedean