Theorems · Theorem · order theory

iUnion_Ioc_map_succ_eq_Ioi

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] [inst_4 : LinearOrder β] {f : α → β},
  (∀ (a : α), f ⊥ ≤ f a) → ¬BddAbove (Set.range f) → ⋃ a, Set.Ioc (f a) (f (Order.succ a)) = Set.Ioi (f ⊥)

Special case a = ⊥ of biUnion_Ici_Ioc_map_succ.

Defined in

Mathlib.Order.SuccPred.IntervalSucc

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderOrderBotSuccOrderIsSuccArchimedeanLinearOrder