Theorems · Theorem · order theory

StrictMonoOn.Iic_union_Ici

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
  StrictMonoOn f (Set.Iic a) → StrictMonoOn f (Set.Ici a) → StrictMono f

If f is strictly monotone both on (-∞, a] and [a, ∞), then it is strictly monotone on the whole line.

Defined in

Mathlib.Order.Monotone.Union

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPreorder