Theorems · Theorem · order theory

Set.Ico_add_one_right_eq_Icc_of_not_isMax

∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Set.Ico a (b + 1) = Set.Icc a b

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

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.Iccstatement and proof · cited by 1,702
Set.Icostatement and proof · cited by 799
IsMaxstatement and proof · cited by 372
Order.succ_eq_add_oneproof · cited by 115
SuccAddOrderstatement and proof · cited by 108
Set.Ico_succ_right_eq_Icc_of_not_isMaxproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.