Theorems · Theorem · order theory

Set.Ioo_add_one_right_eq_Ioc

∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α),
  Set.Ioo a (b + 1) = Set.Ioc a b

Defined in: Mathlib.Algebra.Order.Interval.Set.SuccPred
Cited by: 0 results in Mathlib
Foundations: Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder One Add SuccAddOrder NoMaxOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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.Ioostatement and proof · cited by 1,214
Set.Iocstatement and proof · cited by 971
NoMaxOrderstatement and proof · cited by 340
Order.succ_eq_add_oneproof · cited by 115
SuccAddOrderstatement and proof · cited by 108
Set.Ioo_succ_right_eq_Iocproof · cited by 1

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.