Theorems · Theorem · order theory

iUnion_Ico_map_succ_eq_Ici

∀ {α : 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.Ico (f a) (f (Order.succ a)) = Set.Ici (f ⊥)

Special case a = ⊥ of biUnion_Ici_Ico_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: LinearOrder OrderBot SuccOrder IsSuccArchimedean LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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.imageproof · cited by 5,609
Bot.botstatement and proof · cited by 4,720
Set.rangestatement and proof · cited by 4,705
Set.iUnionstatement and proof · cited by 2,483
Set.Icistatement and proof · cited by 1,070
OrderBotstatement and proof · cited by 1,055
Set.Icostatement and proof · cited by 799
Order.succstatement and proof · cited by 633
BddAbovestatement and proof · cited by 620
SuccOrderstatement and proof · cited by 574

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.