Theorems · Theorem · order theory

biUnion_Ici_Ico_map_succ

∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α]
  [inst_3 : LinearOrder β] {f : α → β} {a : α},
  (∀ i ∈ Set.Ici a, f a ≤ f i) →
    ¬BddAbove (f '' Set.Ici a) → ⋃ i ∈ Set.Ici a, Set.Ico (f i) (f (Order.succ i)) = Set.Ici (f a)

Union formula for Set.Ico (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_Ico_map_succ_eq_Ici for the specialization a = ⊥.

Defined in

Mathlib.Order.SuccPred.IntervalSucc

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderIsSuccArchimedeanLinearOrder