Theorems · Theorem · order theory

StrictMonoOn.Iic_id_le

∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [OrderBot α] {n : α} {φ : α → α},
  StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ 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

LinearOrderSuccOrderIsSuccArchimedeanOrderBot