Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module order.succ_pred.interval_succ
! 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.4955LinearOrder α: 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.20SuccOrder α: Type ?u.11α] [IsSuccArchimedean: (α : Type ?u.167) → [inst : Preorder α] → [inst : SuccOrder α] → PropIsSuccArchimedean α: Type ?u.11α] [LinearOrder: Type ?u.281 → Type ?u.281LinearOrder β: Type ?u.14β] {f: α → βf : α: Type ?u.11α → β: Type ?u.14β}
(hf: Monotone fhf : Monotone: {α : Type ?u.289} → {β : Type ?u.288} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) (m: αm n: αn : α: Type ?u.11α) : (⋃ i: ?m.586i ∈ Ico: {α : Type ?u.611} → [inst : Preorder α] → α → α → Set αIco m: αm n: αn, Ioc: {α : Type ?u.644} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf i: ?m.586i) (f: α → βf (succ: {α : Type ?u.665} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc i: ?m.586i))) = Ioc: {α : Type ?u.700} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf m: αm) (f: α → βf n: αn) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, 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 ≤ ale_total n: αn m: αm with hnm: ?m.747hnm hmn: ?m.748hmnα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)
α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: α(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)rw [α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(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.747hnm,α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(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 fhf hnm: ?m.747hnm),α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = ∅ α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhnm: n ≤ minl∅ = ∅]Goals accomplished! 🐙
α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: α(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n) α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(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 nSucc.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.748hmnα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m)α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m) α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.refine'_1(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f m)α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr(iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f n)·α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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 ≤ khmk ihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)ihkα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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 cIoc_union_Ioc_eq_Ioc (hf: Monotone fhf hmk: m ≤ khmk) (hf: Monotone fhf <| le_succ: ∀ {α : Type ?u.1677} [inst : Preorder α] [inst_1 : SuccOrder α] (a : α), a ≤ succ ale_succ _: ?m.1678_),α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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 ∪ aunion_comm,α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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.1917hk : IsMax: {α : Type ?u.1751} → [inst : LE α] → α → PropIsMax k: αkα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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.1910hk.succ_eq: ∀ {α : Type ?u.1924} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α}, IsMax a → succ a = asucc_eq,α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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 = aempty_unionα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: IsMax kpos(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ ninr.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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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 ≤ khmk hk: ?m.1917hk,α: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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 xbiUnion_insertα: Type u_1β: Type u_2inst✝³: LinearOrder αinst✝²: SuccOrder αinst✝¹: IsSuccArchimedean αinst✝: LinearOrder βf: α → βhf: Monotone fm, n: αhmn: m ≤ nk: αhmk: m ≤ kihk: (iUnion fun i => iUnion fun h => Ioc (f i) (f (succ i))) = Ioc (f m) (f k)hk: ¬IsMax kneg(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.2466SuccOrder α: Type ?u.2457α] [Preorder: Type ?u.2613 → Type ?u.2613Preorder β: Type ?u.2460β] {f: α → βf : α: Type ?u.2457α → β: Type ?u.2460β} (hf: Monotone fhf : Monotone: {α : Type ?u.2621} → {β : Type ?u.2620} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.2765} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.2777} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.2857n => Ioc: {α : Type ?u.2859} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf n: ?m.2857n) (f: α → βf (succ: {α : Type ?u.2877} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.2857n))) :=
(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 → a2 fun _: ?m.3119_ _: ?m.3122_ hmn: ?m.3125hmn =>
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 → ampr 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 ≤ anot_le <| h₁: x✝¹ ≤ f (succ x✝³)h₁.trans: ∀ {α : Type ?u.3246} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ ctrans <| hf: Monotone fhf <| succ_le_of_lt: ∀ {α : Type ?u.3266} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → succ a ≤ bsucc_le_of_lt hmn: ?m.3125hmn
#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.3716SuccOrder α: Type ?u.3707α] [Preorder: Type ?u.3863 → Type ?u.3863Preorder β: Type ?u.3710β] {f: α → βf : α: Type ?u.3707α → β: Type ?u.3710β} (hf: Monotone fhf : Monotone: {α : Type ?u.3871} → {β : Type ?u.3870} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.4015} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.4027} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.4107n => Ico: {α : Type ?u.4109} → [inst : Preorder α] → α → α → Set αIco (f: α → βf n: ?m.4107n) (f: α → βf (succ: {α : Type ?u.4127} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.4107n))) :=
(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 → a2 fun _: ?m.4369_ _: ?m.4372_ hmn: ?m.4375hmn =>
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 → ampr 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 ≤ anot_le <| (hf: Monotone fhf <| succ_le_of_lt: ∀ {α : Type ?u.4498} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → succ a ≤ bsucc_le_of_lt hmn: ?m.4375hmn).trans: ∀ {α : Type ?u.4696} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ ctrans 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.4958SuccOrder α: Type ?u.4949α] [Preorder: Type ?u.5105 → Type ?u.5105Preorder β: Type ?u.4952β] {f: α → βf : α: Type ?u.4949α → β: Type ?u.4952β} (hf: Monotone fhf : Monotone: {α : Type ?u.5113} → {β : Type ?u.5112} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.5257} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.5269} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.5349n => Ioo: {α : Type ?u.5351} → [inst : Preorder α] → α → α → Set αIoo (f: α → βf n: ?m.5349n) (f: α → βf (succ: {α : Type ?u.5369} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.5349n))) :=
hf: Monotone fhf.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 pmono fun _: ?m.5561_ _: ?m.5564_ h: ?m.5567h => h: ?m.5567h.mono: ∀ {α : Type ?u.5569} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b c d : α},
a ≤ b → c ≤ d → Disjoint b d → Disjoint a cmono Ioo_subset_Ico_self: ∀ {α : Type ?u.5638} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ico a bIoo_subset_Ico_self Ioo_subset_Ico_self: ∀ {α : Type ?u.5676} [inst : Preorder α] {a b : α}, Ioo a b ⊆ Ico a bIoo_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.5799PredOrder α: Type ?u.5790α] [Preorder: Type ?u.5946 → Type ?u.5946Preorder β: Type ?u.5793β] {f: α → βf : α: Type ?u.5790α → β: Type ?u.5793β} (hf: Monotone fhf : Monotone: {α : Type ?u.5954} → {β : Type ?u.5953} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.6098} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.6110} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.6190n => Ioc: {α : Type ?u.6192} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf (pred: {α : Type ?u.6210} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.6190n)) (f: α → βf n: ?m.6190n)) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝²: LinearOrder αinst✝¹: PredOrder αinst✝: Preorder βf: α → βhf: Monotone fPairwise (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 adual_Ico] using hf: Monotone fhf.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_succGoals 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.7089PredOrder α: Type ?u.7080α] [Preorder: Type ?u.7236 → Type ?u.7236Preorder β: Type ?u.7083β] {f: α → βf : α: Type ?u.7080α → β: Type ?u.7083β} (hf: Monotone fhf : Monotone: {α : Type ?u.7244} → {β : Type ?u.7243} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.7388} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.7400} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.7480n => Ico: {α : Type ?u.7482} → [inst : Preorder α] → α → α → Set αIco (f: α → βf (pred: {α : Type ?u.7500} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.7480n)) (f: α → βf n: ?m.7480n)) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝²: LinearOrder αinst✝¹: PredOrder αinst✝: Preorder βf: α → βhf: Monotone fPairwise (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 adual_Ioc] using hf: Monotone fhf.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_succGoals 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.8379PredOrder α: Type ?u.8370α] [Preorder: Type ?u.8526 → Type ?u.8526Preorder β: Type ?u.8373β] {f: α → βf : α: Type ?u.8370α → β: Type ?u.8373β} (hf: Monotone fhf : Monotone: {α : Type ?u.8534} → {β : Type ?u.8533} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropMonotone f: α → βf) :
Pairwise: {α : Type ?u.8678} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.8690} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.8770n => Ioo: {α : Type ?u.8772} → [inst : Preorder α] → α → α → Set αIoo (f: α → βf (pred: {α : Type ?u.8790} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.8770n)) (f: α → βf n: ?m.8770n)) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2inst✝²: LinearOrder αinst✝¹: PredOrder αinst✝: Preorder βf: α → βhf: Monotone fPairwise (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 adual_Ioo] using hf: Monotone fhf.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_succGoals 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.9654SuccOrder α: Type ?u.9645α] [Preorder: Type ?u.9801 → Type ?u.9801Preorder β: Type ?u.9648β] {f: α → βf : α: Type ?u.9645α → β: Type ?u.9648β} (hf: Antitone fhf : Antitone: {α : Type ?u.9809} → {β : Type ?u.9808} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.9953} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.9965} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.10045n => Ioc: {α : Type ?u.10047} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf (succ: {α : Type ?u.10065} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.10045n)) (f: α → βf n: ?m.10045n)) :=
hf: Antitone fhf.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.10488SuccOrder α: Type ?u.10479α] [Preorder: Type ?u.10635 → Type ?u.10635Preorder β: Type ?u.10482β] {f: α → βf : α: Type ?u.10479α → β: Type ?u.10482β} (hf: Antitone fhf : Antitone: {α : Type ?u.10643} → {β : Type ?u.10642} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.10787} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.10799} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.10879n => Ico: {α : Type ?u.10881} → [inst : Preorder α] → α → α → Set αIco (f: α → βf (succ: {α : Type ?u.10899} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.10879n)) (f: α → βf n: ?m.10879n)) :=
hf: Antitone fhf.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.11322SuccOrder α: Type ?u.11313α] [Preorder: Type ?u.11469 → Type ?u.11469Preorder β: Type ?u.11316β] {f: α → βf : α: Type ?u.11313α → β: Type ?u.11316β} (hf: Antitone fhf : Antitone: {α : Type ?u.11477} → {β : Type ?u.11476} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.11621} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.11633} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.11713n => Ioo: {α : Type ?u.11715} → [inst : Preorder α] → α → α → Set αIoo (f: α → βf (succ: {α : Type ?u.11733} → [inst : Preorder α] → [inst : SuccOrder α] → α → αsucc n: ?m.11713n)) (f: α → βf n: ?m.11713n)) :=
hf: Antitone fhf.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.12156PredOrder α: Type ?u.12147α] [Preorder: Type ?u.12303 → Type ?u.12303Preorder β: Type ?u.12150β] {f: α → βf : α: Type ?u.12147α → β: Type ?u.12150β} (hf: Antitone fhf : Antitone: {α : Type ?u.12311} → {β : Type ?u.12310} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.12455} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.12467} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.12547n => Ioc: {α : Type ?u.12549} → [inst : Preorder α] → α → α → Set αIoc (f: α → βf n: ?m.12547n) (f: α → βf (pred: {α : Type ?u.12567} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.12547n))) :=
hf: Antitone fhf.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.12990PredOrder α: Type ?u.12981α] [Preorder: Type ?u.13137 → Type ?u.13137Preorder β: Type ?u.12984β] {f: α → βf : α: Type ?u.12981α → β: Type ?u.12984β} (hf: Antitone fhf : Antitone: {α : Type ?u.13145} → {β : Type ?u.13144} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.13289} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.13301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.13381n => Ico: {α : Type ?u.13383} → [inst : Preorder α] → α → α → Set αIco (f: α → βf n: ?m.13381n) (f: α → βf (pred: {α : Type ?u.13401} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.13381n))) :=
hf: Antitone fhf.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.13824PredOrder α: Type ?u.13815α] [Preorder: Type ?u.13971 → Type ?u.13971Preorder β: Type ?u.13818β] {f: α → βf : α: Type ?u.13815α → β: Type ?u.13818β} (hf: Antitone fhf : Antitone: {α : Type ?u.13979} → {β : Type ?u.13978} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → PropAntitone f: α → βf) :
Pairwise: {α : Type ?u.14123} → (α → α → Prop) → PropPairwise (Disjoint: {α : Type ?u.14135} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → PropDisjoint on fun n: ?m.14215n => Ioo: {α : Type ?u.14217} → [inst : Preorder α] → α → α → Set αIoo (f: α → βf n: ?m.14215n) (f: α → βf (pred: {α : Type ?u.14235} → [inst : Preorder α] → [inst : PredOrder α] → α → αpred n: ?m.14215n))) :=
hf: Antitone fhf.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
```