theorem Set.Ico_subset_Ici {α : Type u_1} {a b c : α} [Preorder α] (h : c ≤ a) : Ico a b ⊆ Ici c

theorem Set.Icc_subset_Ici {α : Type u_1} {a b c : α} [Preorder α] (h : c ≤ a) : Icc a b ⊆ Ici c

theorem Set.Ioc_subset_Ioi {α : Type u_1} {a b c : α} [Preorder α] (h : c ≤ a) : Ioc a b ⊆ Ioi c

theorem Set.Ioo_subset_Ioi {α : Type u_1} {a b c : α} [Preorder α] (h : c ≤ a) : Ioo a b ⊆ Ioi c

theorem Set.iUnion_Ico_eq_Ici {α : Type u_1} [LinearOrder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f 0 ≤ f n) (h2f : ¬BddAbove (range f)) : ⋃ (i : ℕ), Ico (f i) (f (i + 1)) = Ici (f 0)

theorem Set.iUnion_Ioc_eq_Ioi {α : Type u_1} [LinearOrder α] {f : ℕ → α} (hf : ∀ (n : ℕ), f 0 ≤ f n) (h2f : ¬BddAbove (range f)) : ⋃ (i : ℕ), Ioc (f i) (f (i + 1)) = Ioi (f 0)

theorem Set.pairwise_disjoint_Ico_monotone {α : Type u_1} [LinearOrder α] {ι : Type u_2} [LinearOrder ι] [SuccOrder ι] {f : ι → α} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (i : ι) => Ico (f i) (f (Order.succ i)))

theorem Set.pairwise_disjoint_Ioc_monotone {α : Type u_1} [LinearOrder α] {ι : Type u_2} [LinearOrder ι] [SuccOrder ι] {f : ι → α} (hf : Monotone f) : Pairwise (Function.onFun Disjoint fun (i : ι) => Ioc (f i) (f (Order.succ i)))