/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module order.succ_pred.interval_succ
! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Pairwise.Basic
import Mathlib.Order.SuccPred.Basic

/-!
# Intervals `Ixx (f x) (f (Order.succ x))`

In this file we prove

* `Monotone.biUnion_Ico_Ioc_map_succ`: if `α` is a linear archimedean succ order and `β` is a linear
  order, then for any monotone function `f` and `m n : α`, the union of intervals
  `Set.Ioc (f i) (f (Order.succ i))`, `m ≤ i < n`, is equal to `Set.Ioc (f m) (f n)`;

* `Monotone.pairwise_disjoint_on_Ioc_succ`: if `α` is a linear succ order, `β` is a preorder, and
  `f : α → β` is a monotone function, then the intervals `Set.Ioc (f n) (f (Order.succ n))` are
  pairwise disjoint.

For the latter lemma, we also prove various order dual versions.
-/


open Set Order

variable {α: Type ?u.2
α β: Type ?u.3710
β : Type _: Type (?u.5793+1)
Type _} [LinearOrder: Type ?u.4955 → Type ?u.4955
LinearOrder α: Type ?u.8370
α]

namespace Monotone

/-- If `α` is a linear archimedean succ order and `β` is a linear order, then for any monotone
function `f` and `m n : α`, the union of intervals `Set.Ioc (f i) (f (Order.succ i))`, `m ≤ i < n`,
is equal to `Set.Ioc (f m) (f n)` -/
theorem biUnion_Ico_Ioc_map_succ: ∀ [inst : SuccOrder α] [inst_1 : IsSuccArchimedean α] [inst_2 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (m n : α), (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
biUnion_Ico_Ioc_map_succ [SuccOrder: (α : Type ?u.20) → [inst : Preorder α] → Type ?u.20
SuccOrder α: Type ?u.11
α] [IsSuccArchimedean: (α : Type ?u.167) → [inst : Preorder α] → [inst : SuccOrder α] → Prop
IsSuccArchimedean α: Type ?u.11
α] [LinearOrder: Type ?u.281 → Type ?u.281
LinearOrder β: Type ?u.14
β] {f: α → β
f : α: Type ?u.11
α → β: Type ?u.14
β}
    (hf: Monotone f
hf : Monotone: {α : Type ?u.289} → {β : Type ?u.288} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) (m: α
m n: α
n : α: Type ?u.11
α) : (⋃ i: ?m.586
i ∈ Ico: {α : Type ?u.611} → [inst : Preorder α] → α → α → Set α
Ico m: α
m n: α
n, Ioc: {α : Type ?u.644} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f i: ?m.586
i) (f: α → β
f (succ: {α : Type ?u.665} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ i: ?m.586
i))) = Ioc: {α : Type ?u.700} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f m: α
m) (f: α → β
f n: α
n) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)cases' le_total: ∀ {α : Type ?u.715} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
le_total n: α
n m: α
m with hnm: ?m.747
hnm hmn: ?m.748
hmnα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
  α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)rw [α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)Ico_eq_empty_of_le: ∀ {α : Type ?u.790} [inst : Preorder α] {a b : α}, b ≤ a → Ico a b = ∅
Ico_eq_empty_of_le hnm: ?m.747
hnm,α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)Ioc_eq_empty_of_le: ∀ {α : Type ?u.950} [inst : Preorder α] {a b : α}, b ≤ a → Ioc a b = ∅
Ioc_eq_empty_of_le (hf: Monotone f
hf hnm: ?m.747
hnm),α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = ∅ α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)biUnion_empty: ∀ {α : Type ?u.1114} {β : Type ?u.1113} (s : α → Set β), (iUnion fun x => iUnion fun h => s x) = ∅
biUnion_emptyα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hnm: n ≤ m

inl∅ = ∅]
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)refine' Succ.rec: ∀ {α : Type ?u.1148} [inst : Preorder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α] {P : α → Prop} {m : α},
  P m → (∀ (n : α), m ≤ n → P n → P (succ n)) → ∀ ⦃n : α⦄, m ≤ n → P n
Succ.rec _: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m)
_ _: ∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))
_ hmn: ?m.748
hmnα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m)
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))
    α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m)
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))simp only [Ioc_self: ∀ {α : Type ?u.1219} [inst : Preorder α] (a : α), Ioc a a = ∅
Ioc_self, Ico_self: ∀ {α : Type ?u.1231} [inst : Preorder α] (a : α), Ico a a = ∅
Ico_self, biUnion_empty: ∀ {α : Type ?u.1244} {β : Type ?u.1243} (s : α → Set β), (iUnion fun x => iUnion fun h => s x) = ∅
biUnion_empty]
Goals accomplished! 🐙
    α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))intro k: α
k hmk: m ≤ k
hmk ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)
ihkα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ k))
      α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))rw [α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ k))← Ioc_union_Ioc_eq_Ioc: ∀ {α : Type ?u.1634} [inst : LinearOrder α] {a b c : α}, a ≤ b → b ≤ c → Ioc a b ∪ Ioc b c = Ioc a c
Ioc_union_Ioc_eq_Ioc (hf: Monotone f
hf hmk: m ≤ k
hmk) (hf: Monotone f
hf <| le_succ: ∀ {α : Type ?u.1677} [inst : Preorder α] [inst_1 : SuccOrder α] (a : α), a ≤ succ a
le_succ _: ?m.1678
_),α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k) ∪ Ioc (f k) (f (succ k)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ k))union_comm: ∀ {α : Type ?u.1713} (a b : Set α), a ∪ b = b ∪ a
union_comm,α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f k) (f (succ k)) ∪ Ioc (f m) (f k) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ k))← ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)
ihkα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))]α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

inr.refine'_2(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))
      α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))by_cases hk: ?m.1917
hk : IsMax: {α : Type ?u.1751} → [inst : LE α] → α → Prop
IsMax k: α
kα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))
      α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))
α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))rw [α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))hk: ?m.1910
hk.succ_eq: ∀ {α : Type ?u.1924} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α}, IsMax a → succ a = a
succ_eq,α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f k) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))Ioc_self: ∀ {α : Type ?u.2091} [inst : Preorder α] (a : α), Ioc a a = ∅
Ioc_self,α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = ∅ ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))empty_union: ∀ {α : Type ?u.2278} (a : Set α), ∅ ∪ a = a
empty_unionα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: IsMax k

pos(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))]
Goals accomplished! 🐙
      α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

inr.refine'_2∀ (n : α),
  m ≤ n →
    (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) →
      (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f (succ n))·α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))rw [α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))Ico_succ_right_eq_insert_of_not_isMax: ∀ {α : Type ?u.2301} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → Ico a (succ b) = insert b (Ico a b)
Ico_succ_right_eq_insert_of_not_isMax hmk: m ≤ k
hmk hk: ?m.1917
hk,α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i)) α: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))biUnion_insert: ∀ {α : Type ?u.2330} {β : Type ?u.2331} (a : α) (s : Set α) (t : α → Set β),
  (iUnion fun x => iUnion fun h => t x) = t a ∪ iUnion fun x => iUnion fun h => t x
biUnion_insertα: Type u_1

β: Type u_2

inst✝³: LinearOrder α

inst✝²: SuccOrder α

inst✝¹: IsSuccArchimedean α

inst✝: LinearOrder β

f: α → β

hf: Monotone f

m, n: α

hmn: m ≤ n

k: α

hmk: m ≤ k

ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)

hk: ¬IsMax k

neg(Ioc (f k) (f (succ k)) ∪ iUnion fun x => iUnion fun h => Ioc (f x) (f (succ x))) =   Ioc (f k) (f (succ k)) ∪ iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))]
Goals accomplished! 🐙
#align monotone.bUnion_Ico_Ioc_map_succ Monotone.biUnion_Ico_Ioc_map_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : IsSuccArchimedean α]
  [inst_3 : LinearOrder β] {f : α → β},
  Monotone f → ∀ (m n : α), (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
Monotone.biUnion_Ico_Ioc_map_succ

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioc (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioc_succ: ∀ [inst : SuccOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (succ n)))
pairwise_disjoint_on_Ioc_succ [SuccOrder: (α : Type ?u.2466) → [inst : Preorder α] → Type ?u.2466
SuccOrder α: Type ?u.2457
α] [Preorder: Type ?u.2613 → Type ?u.2613
Preorder β: Type ?u.2460
β] {f: α → β
f : α: Type ?u.2457
α → β: Type ?u.2460
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.2621} → {β : Type ?u.2620} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.2765} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.2777} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.2857
n => Ioc: {α : Type ?u.2859} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f n: ?m.2857
n) (f: α → β
f (succ: {α : Type ?u.2877} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.2857
n))) :=
  (pairwise_disjoint_on: ∀ {α : Type ?u.3002} {ι : Type ?u.3003} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : LinearOrder ι]
  (f : ι → α), Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
pairwise_disjoint_on _: ?m.3005 → ?m.3004
_).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun _: ?m.3119
_ _: ?m.3122
_ hmn: ?m.3125
hmn =>
    disjoint_iff_inf_le: ∀ {α : Type ?u.3127} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b ≤ ⊥
disjoint_iff_inf_le.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr fun _: ?m.3174
_ ⟨⟨_, h₁: x✝¹ ≤ f (succ x✝³)
h₁⟩, ⟨h₂: f x✝² < x✝¹
h₂, _⟩⟩ =>
      h₂: f x✝² < x✝¹
h₂.not_le: ∀ {α : Type ?u.3229} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le <| h₁: x✝¹ ≤ f (succ x✝³)
h₁.trans: ∀ {α : Type ?u.3246} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| hf: Monotone f
hf <| succ_le_of_lt: ∀ {α : Type ?u.3266} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → succ a ≤ b
succ_le_of_lt hmn: ?m.3125
hmn
#align monotone.pairwise_disjoint_on_Ioc_succ Monotone.pairwise_disjoint_on_Ioc_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (succ n)))
Monotone.pairwise_disjoint_on_Ioc_succ

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ico (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_succ: ∀ [inst : SuccOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f n) (f (succ n)))
pairwise_disjoint_on_Ico_succ [SuccOrder: (α : Type ?u.3716) → [inst : Preorder α] → Type ?u.3716
SuccOrder α: Type ?u.3707
α] [Preorder: Type ?u.3863 → Type ?u.3863
Preorder β: Type ?u.3710
β] {f: α → β
f : α: Type ?u.3707
α → β: Type ?u.3710
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.3871} → {β : Type ?u.3870} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.4015} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.4027} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.4107
n => Ico: {α : Type ?u.4109} → [inst : Preorder α] → α → α → Set α
Ico (f: α → β
f n: ?m.4107
n) (f: α → β
f (succ: {α : Type ?u.4127} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.4107
n))) :=
  (pairwise_disjoint_on: ∀ {α : Type ?u.4252} {ι : Type ?u.4253} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : LinearOrder ι]
  (f : ι → α), Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
pairwise_disjoint_on _: ?m.4255 → ?m.4254
_).2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 fun _: ?m.4369
_ _: ?m.4372
_ hmn: ?m.4375
hmn =>
    disjoint_iff_inf_le: ∀ {α : Type ?u.4377} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b ≤ ⊥
disjoint_iff_inf_le.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr fun _: ?m.4424
_ ⟨⟨_, h₁: x✝¹ < f (succ x✝³)
h₁⟩, ⟨h₂: f x✝² ≤ x✝¹
h₂, _⟩⟩ =>
      h₁: x✝¹ < f (succ x✝³)
h₁.not_le: ∀ {α : Type ?u.4479} [inst : Preorder α] {a b : α}, a < b → ¬b ≤ a
not_le <| (hf: Monotone f
hf <| succ_le_of_lt: ∀ {α : Type ?u.4498} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → succ a ≤ b
succ_le_of_lt hmn: ?m.4375
hmn).trans: ∀ {α : Type ?u.4696} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans h₂: f x✝² ≤ x✝¹
h₂
#align monotone.pairwise_disjoint_on_Ico_succ Monotone.pairwise_disjoint_on_Ico_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f n) (f (succ n)))
Monotone.pairwise_disjoint_on_Ico_succ

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioo (f n) (f (Order.succ n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioo_succ: ∀ [inst : SuccOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (succ n)))
pairwise_disjoint_on_Ioo_succ [SuccOrder: (α : Type ?u.4958) → [inst : Preorder α] → Type ?u.4958
SuccOrder α: Type ?u.4949
α] [Preorder: Type ?u.5105 → Type ?u.5105
Preorder β: Type ?u.4952
β] {f: α → β
f : α: Type ?u.4949
α → β: Type ?u.4952
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.5113} → {β : Type ?u.5112} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.5257} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.5269} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.5349
n => Ioo: {α : Type ?u.5351} → [inst : Preorder α] → α → α → Set α
Ioo (f: α → β
f n: ?m.5349
n) (f: α → β
f (succ: {α : Type ?u.5369} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.5349
n))) :=
  hf: Monotone f
hf.pairwise_disjoint_on_Ico_succ: ∀ {α : Type ?u.5494} {β : Type ?u.5495} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f n) (f (succ n)))
pairwise_disjoint_on_Ico_succ.mono: ∀ {α : Type ?u.5537} {r p : α → α → Prop}, Pairwise r → (∀ ⦃i j : α⦄, r i j → p i j) → Pairwise p
mono fun _: ?m.5561
_ _: ?m.5564
_ h: ?m.5567
h => h: ?m.5567
h.mono: ∀ {α : Type ?u.5569} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
  a ≤ b → c ≤ d → Disjoint b d → Disjoint a c
mono Ioo_subset_Ico_self: ∀ {α : Type ?u.5638} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ico a b
Ioo_subset_Ico_self Ioo_subset_Ico_self: ∀ {α : Type ?u.5676} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ico a b
Ioo_subset_Ico_self
#align monotone.pairwise_disjoint_on_Ioo_succ Monotone.pairwise_disjoint_on_Ioo_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (succ n)))
Monotone.pairwise_disjoint_on_Ioo_succ

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioc (f Order.pred n) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioc_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))
pairwise_disjoint_on_Ioc_pred [PredOrder: (α : Type ?u.5799) → [inst : Preorder α] → Type ?u.5799
PredOrder α: Type ?u.5790
α] [Preorder: Type ?u.5946 → Type ?u.5946
Preorder β: Type ?u.5793
β] {f: α → β
f : α: Type ?u.5790
α → β: Type ?u.5793
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.5954} → {β : Type ?u.5953} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.6098} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.6110} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.6190
n => Ioc: {α : Type ?u.6192} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f (pred: {α : Type ?u.6210} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.6190
n)) (f: α → β
f n: ?m.6190
n)) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

inst✝²: LinearOrder α

inst✝¹: PredOrder α

inst✝: Preorder β

f: α → β

hf: Monotone f

Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))simpa only [(· ∘ ·), dual_Ico: ∀ {α : Type ?u.6360} [inst : Preorder α] {a b : α},
  Ico (↑OrderDual.toDual a) (↑OrderDual.toDual b) = ↑OrderDual.ofDual ⁻¹' Ioc b a
dual_Ico] using hf: Monotone f
hf.dual: ∀ {α : Type ?u.6483} {β : Type ?u.6482} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.pairwise_disjoint_on_Ico_succ: ∀ {α : Type ?u.6641} {β : Type ?u.6642} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f n) (f (succ n)))
pairwise_disjoint_on_Ico_succ
Goals accomplished! 🐙
#align monotone.pairwise_disjoint_on_Ioc_pred Monotone.pairwise_disjoint_on_Ioc_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))
Monotone.pairwise_disjoint_on_Ioc_pred

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ico (f Order.pred n) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_pred: ∀ [inst : PredOrder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))
pairwise_disjoint_on_Ico_pred [PredOrder: (α : Type ?u.7089) → [inst : Preorder α] → Type ?u.7089
PredOrder α: Type ?u.7080
α] [Preorder: Type ?u.7236 → Type ?u.7236
Preorder β: Type ?u.7083
β] {f: α → β
f : α: Type ?u.7080
α → β: Type ?u.7083
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.7244} → {β : Type ?u.7243} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.7388} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.7400} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.7480
n => Ico: {α : Type ?u.7482} → [inst : Preorder α] → α → α → Set α
Ico (f: α → β
f (pred: {α : Type ?u.7500} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.7480
n)) (f: α → β
f n: ?m.7480
n)) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

inst✝²: LinearOrder α

inst✝¹: PredOrder α

inst✝: Preorder β

f: α → β

hf: Monotone f

Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))simpa only [(· ∘ ·), dual_Ioc: ∀ {α : Type ?u.7650} [inst : Preorder α] {a b : α},
  Ioc (↑OrderDual.toDual a) (↑OrderDual.toDual b) = ↑OrderDual.ofDual ⁻¹' Ico b a
dual_Ioc] using hf: Monotone f
hf.dual: ∀ {α : Type ?u.7773} {β : Type ?u.7772} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.pairwise_disjoint_on_Ioc_succ: ∀ {α : Type ?u.7931} {β : Type ?u.7932} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (succ n)))
pairwise_disjoint_on_Ioc_succ
Goals accomplished! 🐙
#align monotone.pairwise_disjoint_on_Ico_pred Monotone.pairwise_disjoint_on_Ico_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))
Monotone.pairwise_disjoint_on_Ico_pred

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioo (f Order.pred n) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioo_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))
pairwise_disjoint_on_Ioo_pred [PredOrder: (α : Type ?u.8379) → [inst : Preorder α] → Type ?u.8379
PredOrder α: Type ?u.8370
α] [Preorder: Type ?u.8526 → Type ?u.8526
Preorder β: Type ?u.8373
β] {f: α → β
f : α: Type ?u.8370
α → β: Type ?u.8373
β} (hf: Monotone f
hf : Monotone: {α : Type ?u.8534} → {β : Type ?u.8533} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone f: α → β
f) :
    Pairwise: {α : Type ?u.8678} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.8690} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.8770
n => Ioo: {α : Type ?u.8772} → [inst : Preorder α] → α → α → Set α
Ioo (f: α → β
f (pred: {α : Type ?u.8790} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.8770
n)) (f: α → β
f n: ?m.8770
n)) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type u_2

inst✝²: LinearOrder α

inst✝¹: PredOrder α

inst✝: Preorder β

f: α → β

hf: Monotone f

Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))simpa only [(· ∘ ·), dual_Ioo: ∀ {α : Type ?u.8940} [inst : Preorder α] {a b : α},
  Ioo (↑OrderDual.toDual a) (↑OrderDual.toDual b) = ↑OrderDual.ofDual ⁻¹' Ioo b a
dual_Ioo] using hf: Monotone f
hf.dual: ∀ {α : Type ?u.9063} {β : Type ?u.9062} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (↑OrderDual.toDual ∘ f ∘ ↑OrderDual.ofDual)
dual.pairwise_disjoint_on_Ioo_succ: ∀ {α : Type ?u.9221} {β : Type ?u.9222} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (succ n)))
pairwise_disjoint_on_Ioo_succ
Goals accomplished! 🐙
#align monotone.pairwise_disjoint_on_Ioo_pred Monotone.pairwise_disjoint_on_Ioo_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))
Monotone.pairwise_disjoint_on_Ioo_pred

end Monotone

namespace Antitone

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioc (f (Order.succ n)) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioc_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioc (f (succ n)) (f n))
pairwise_disjoint_on_Ioc_succ [SuccOrder: (α : Type ?u.9654) → [inst : Preorder α] → Type ?u.9654
SuccOrder α: Type ?u.9645
α] [Preorder: Type ?u.9801 → Type ?u.9801
Preorder β: Type ?u.9648
β] {f: α → β
f : α: Type ?u.9645
α → β: Type ?u.9648
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.9809} → {β : Type ?u.9808} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.9953} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.9965} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.10045
n => Ioc: {α : Type ?u.10047} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f (succ: {α : Type ?u.10065} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.10045
n)) (f: α → β
f n: ?m.10045
n)) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.10191} {β : Type ?u.10190} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ioc_pred: ∀ {α : Type ?u.10350} {β : Type ?u.10351} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ioc (f (pred n)) (f n))
pairwise_disjoint_on_Ioc_pred
#align antitone.pairwise_disjoint_on_Ioc_succ Antitone.pairwise_disjoint_on_Ioc_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioc (f (succ n)) (f n))
Antitone.pairwise_disjoint_on_Ioc_succ

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ico (f (Order.succ n)) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_succ: ∀ [inst : SuccOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ico (f (succ n)) (f n))
pairwise_disjoint_on_Ico_succ [SuccOrder: (α : Type ?u.10488) → [inst : Preorder α] → Type ?u.10488
SuccOrder α: Type ?u.10479
α] [Preorder: Type ?u.10635 → Type ?u.10635
Preorder β: Type ?u.10482
β] {f: α → β
f : α: Type ?u.10479
α → β: Type ?u.10482
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.10643} → {β : Type ?u.10642} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.10787} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.10799} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.10879
n => Ico: {α : Type ?u.10881} → [inst : Preorder α] → α → α → Set α
Ico (f: α → β
f (succ: {α : Type ?u.10899} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.10879
n)) (f: α → β
f n: ?m.10879
n)) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.11025} {β : Type ?u.11024} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ico_pred: ∀ {α : Type ?u.11184} {β : Type ?u.11185} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ico (f (pred n)) (f n))
pairwise_disjoint_on_Ico_pred
#align antitone.pairwise_disjoint_on_Ico_succ Antitone.pairwise_disjoint_on_Ico_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ico (f (succ n)) (f n))
Antitone.pairwise_disjoint_on_Ico_succ

/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioo (f (Order.succ n)) (f n)` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioo_succ: ∀ [inst : SuccOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioo (f (succ n)) (f n))
pairwise_disjoint_on_Ioo_succ [SuccOrder: (α : Type ?u.11322) → [inst : Preorder α] → Type ?u.11322
SuccOrder α: Type ?u.11313
α] [Preorder: Type ?u.11469 → Type ?u.11469
Preorder β: Type ?u.11316
β] {f: α → β
f : α: Type ?u.11313
α → β: Type ?u.11316
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.11477} → {β : Type ?u.11476} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.11621} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.11633} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.11713
n => Ioo: {α : Type ?u.11715} → [inst : Preorder α] → α → α → Set α
Ioo (f: α → β
f (succ: {α : Type ?u.11733} → [inst : Preorder α] → [inst : SuccOrder α] → α → α
succ n: ?m.11713
n)) (f: α → β
f n: ?m.11713
n)) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.11859} {β : Type ?u.11858} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ioo_pred: ∀ {α : Type ?u.12018} {β : Type ?u.12019} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ioo (f (pred n)) (f n))
pairwise_disjoint_on_Ioo_pred
#align antitone.pairwise_disjoint_on_Ioo_succ Antitone.pairwise_disjoint_on_Ioo_succ: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioo (f (succ n)) (f n))
Antitone.pairwise_disjoint_on_Ioo_succ

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioc (f n) (f (Order.pred n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioc_pred: ∀ [inst : PredOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (pred n)))
pairwise_disjoint_on_Ioc_pred [PredOrder: (α : Type ?u.12156) → [inst : Preorder α] → Type ?u.12156
PredOrder α: Type ?u.12147
α] [Preorder: Type ?u.12303 → Type ?u.12303
Preorder β: Type ?u.12150
β] {f: α → β
f : α: Type ?u.12147
α → β: Type ?u.12150
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.12311} → {β : Type ?u.12310} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.12455} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.12467} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.12547
n => Ioc: {α : Type ?u.12549} → [inst : Preorder α] → α → α → Set α
Ioc (f: α → β
f n: ?m.12547
n) (f: α → β
f (pred: {α : Type ?u.12567} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.12547
n))) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.12693} {β : Type ?u.12692} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ioc_succ: ∀ {α : Type ?u.12852} {β : Type ?u.12853} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (succ n)))
pairwise_disjoint_on_Ioc_succ
#align antitone.pairwise_disjoint_on_Ioc_pred Antitone.pairwise_disjoint_on_Ioc_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioc (f n) (f (pred n)))
Antitone.pairwise_disjoint_on_Ioc_pred

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ico (f n) (f (Order.pred n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ico_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ico (f n) (f (pred n)))
pairwise_disjoint_on_Ico_pred [PredOrder: (α : Type ?u.12990) → [inst : Preorder α] → Type ?u.12990
PredOrder α: Type ?u.12981
α] [Preorder: Type ?u.13137 → Type ?u.13137
Preorder β: Type ?u.12984
β] {f: α → β
f : α: Type ?u.12981
α → β: Type ?u.12984
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.13145} → {β : Type ?u.13144} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.13289} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.13301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.13381
n => Ico: {α : Type ?u.13383} → [inst : Preorder α] → α → α → Set α
Ico (f: α → β
f n: ?m.13381
n) (f: α → β
f (pred: {α : Type ?u.13401} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.13381
n))) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.13527} {β : Type ?u.13526} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ico_succ: ∀ {α : Type ?u.13686} {β : Type ?u.13687} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ico (f n) (f (succ n)))
pairwise_disjoint_on_Ico_succ
#align antitone.pairwise_disjoint_on_Ico_pred Antitone.pairwise_disjoint_on_Ico_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ico (f n) (f (pred n)))
Antitone.pairwise_disjoint_on_Ico_pred

/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is an antitone function, then
the intervals `Set.Ioo (f n) (f (Order.pred n))` are pairwise disjoint. -/
theorem pairwise_disjoint_on_Ioo_pred: ∀ [inst : PredOrder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (pred n)))
pairwise_disjoint_on_Ioo_pred [PredOrder: (α : Type ?u.13824) → [inst : Preorder α] → Type ?u.13824
PredOrder α: Type ?u.13815
α] [Preorder: Type ?u.13971 → Type ?u.13971
Preorder β: Type ?u.13818
β] {f: α → β
f : α: Type ?u.13815
α → β: Type ?u.13818
β} (hf: Antitone f
hf : Antitone: {α : Type ?u.13979} → {β : Type ?u.13978} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone f: α → β
f) :
    Pairwise: {α : Type ?u.14123} → (α → α → Prop) → Prop
Pairwise (Disjoint: {α : Type ?u.14135} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint on fun n: ?m.14215
n => Ioo: {α : Type ?u.14217} → [inst : Preorder α] → α → α → Set α
Ioo (f: α → β
f n: ?m.14215
n) (f: α → β
f (pred: {α : Type ?u.14235} → [inst : Preorder α] → [inst : PredOrder α] → α → α
pred n: ?m.14215
n))) :=
  hf: Antitone f
hf.dual_left: ∀ {α : Type ?u.14361} {β : Type ?u.14360} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (f ∘ ↑OrderDual.ofDual)
dual_left.pairwise_disjoint_on_Ioo_succ: ∀ {α : Type ?u.14520} {β : Type ?u.14521} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β]
  {f : α → β}, Monotone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (succ n)))
pairwise_disjoint_on_Ioo_succ
#align antitone.pairwise_disjoint_on_Ioo_pred Antitone.pairwise_disjoint_on_Ioo_pred: ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Antitone f → Pairwise (Disjoint on fun n => Ioo (f n) (f (pred n)))
Antitone.pairwise_disjoint_on_Ioo_pred

end Antitone