Theorems · Theorem · order theory

biUnion_Ici_Ioc_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.Ioc (f i) (f (Order.succ i)) = Set.Ioi (f a)

Union formula for Set.Ioc (f i) (f (Order.succ i)) over i ∈ Ici a. See also iUnion_Ioc_map_succ_eq_Ioi 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: LinearOrder SuccOrder IsSuccArchimedean LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement · cited by 53,352
LinearOrderstatement and proof · cited by 8,572
Set.ofPredproof · cited by 6,101
Set.imagestatement and proof · cited by 5,609
LE.le.transproof · cited by 3,151
Set.iUnionstatement and proof · cited by 2,483
Set.Ioistatement and proof · cited by 1,463
Set.Icistatement and proof · cited by 1,070
Set.Iocstatement and proof · cited by 971
Order.succstatement and proof · cited by 633
BddAbovestatement and proof · cited by 620
SuccOrderstatement and proof · cited by 574

Cited by1

Results whose statement or proof uses this declaration.

iUnion_Ioc_map_succ_eq_Ioiproof · cited by 0