Theorems · Theorem · order theory

Finset.Ico_union_Ico

∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  min a b ≤ max c d → min c d ≤ max a b → Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)

Defined in

Mathlib.Order.Interval.Finset.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderLocallyFiniteOrder