feat(order/monotone): prove nat.exists_strict_mono etc (#14435)

* add `nat.exists_strict_mono`, `nat.exists_strict_anti`, `int.exists_strict_mono`, and `int.exists_strict_anti`;
* move `set.Iic.no_min_order` and `set.Ici.no_max_order` to `data.set.intervals.basic`;
* add `set.Iio.no_min_order` and `set.Ioi.no_max_order`;
* add `no_max_order.infinite` and `no_min_order.infinite`, use them in the proofs;
* rename `set.Ixx.infinite` to `set.Ixx_infinite`;
* add `set.Ixx.infinite` - lemmas and instances about `infinite`, not `set.infinite`.

src/analysis/special_functions/trigonometric/basic.lean

@@ -481,10 +481,10 @@ subset.antisymm (range_subset_iff.2 cos_mem_Icc) surj_on_cos.subset_range
 subset.antisymm (range_subset_iff.2 sin_mem_Icc) surj_on_sin.subset_range
 
 lemma range_cos_infinite : (range real.cos).infinite :=
-by { rw real.range_cos, exact Icc.infinite (by norm_num) }
+by { rw real.range_cos, exact Icc_infinite (by norm_num) }
 
 lemma range_sin_infinite : (range real.sin).infinite :=
-by { rw real.range_sin, exact Icc.infinite (by norm_num) }
+by { rw real.range_sin, exact Icc_infinite (by norm_num) }
 
 
 section cos_div_sq

src/data/set/intervals/basic.lean

@@ -155,6 +155,18 @@ nonempty.to_subtype nonempty_Ioi
 instance nonempty_Iio_subtype [no_min_order α] : nonempty (Iio a) :=
 nonempty.to_subtype nonempty_Iio
 
+instance [no_min_order α] : no_min_order (Iio a) :=
+⟨λ a, let ⟨b, hb⟩ := exists_lt (a : α) in ⟨⟨b, lt_trans hb a.2⟩, hb⟩⟩
+
+instance [no_min_order α] : no_min_order (Iic a) :=
+⟨λ a, let ⟨b, hb⟩ := exists_lt (a : α) in ⟨⟨b, hb.le.trans a.2⟩, hb⟩⟩
+
+instance [no_max_order α] : no_max_order (Ioi a) :=
+order_dual.no_max_order (Iio (to_dual a))
+
+instance [no_max_order α] : no_max_order (Ici a) :=
+order_dual.no_max_order (Iic (to_dual a))
+
 @[simp] lemma Icc_eq_empty (h : ¬a ≤ b) : Icc a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans hb)
 

src/data/set/intervals/infinite.lean

@@ -9,64 +9,52 @@ import data.set.finite
 # Infinitude of intervals
 
 Bounded intervals in dense orders are infinite, as are unbounded intervals
-in orders that are unbounded on the appropriate side.
+in orders that are unbounded on the appropriate side. We also prove that an unbounded
+preorder is an infinite type.
 -/
 
-namespace set
-
 variables {α : Type*} [preorder α]
 
-section bounded
-
-variables [densely_ordered α]
+/-- A nonempty preorder with no maximal element is infinite. This is not an instance to avoid
+a cycle with `infinite α → nontrivial α → nonempty α`. -/
+lemma no_max_order.infinite [nonempty α] [no_max_order α] : infinite α :=
+let ⟨f, hf⟩ := nat.exists_strict_mono α in infinite.of_injective f hf.injective
 
-lemma Ioo.infinite {a b : α} (h : a < b) : (Ioo a b).infinite :=
-begin
-  rintro (f : finite (Ioo a b)),
-  obtain ⟨m, hm₁, hm₂⟩ : ∃ m ∈ Ioo a b, ∀ x ∈ Ioo a b, ¬x < m,
-  { simpa [h] using finset.exists_minimal f.to_finset },
-  obtain ⟨z, hz₁, hz₂⟩ : ∃ z, a < z ∧ z < m := exists_between hm₁.1,
-  exact hm₂ z ⟨hz₁, lt_trans hz₂ hm₁.2⟩ hz₂,
-end
+/-- A nonempty preorder with no minimal element is infinite. This is not an instance to avoid
+a cycle with `infinite α → nontrivial α → nonempty α`. -/
+lemma no_min_order.infinite [nonempty α] [no_min_order α] : infinite α :=
+@no_max_order.infinite αᵒᵈ _ _ _
 
-lemma Ico.infinite {a b : α} (h : a < b) : (Ico a b).infinite :=
-(Ioo.infinite h).mono Ioo_subset_Ico_self
-
-lemma Ioc.infinite {a b : α} (h : a < b) : (Ioc a b).infinite :=
-(Ioo.infinite h).mono Ioo_subset_Ioc_self
-
-lemma Icc.infinite {a b : α} (h : a < b) : (Icc a b).infinite :=
-(Ioo.infinite h).mono Ioo_subset_Icc_self
+namespace set
 
-end bounded
+section densely_ordered
 
-section unbounded_below
+variables [densely_ordered α] {a b : α} (h : a < b)
 
-variables [no_min_order α]
+lemma Ioo.infinite : infinite (Ioo a b) := @no_max_order.infinite _ _ (nonempty_Ioo_subtype h) _
+lemma Ioo_infinite : (Ioo a b).infinite := infinite_coe_iff.1 $ Ioo.infinite h
 
-lemma Iio.infinite {b : α} : (Iio b).infinite :=
-begin
-  rintro (f : finite (Iio b)),
-  obtain ⟨m, hm₁, hm₂⟩ : ∃ m < b, ∀ x < b, ¬x < m,
-  { simpa using finset.exists_minimal f.to_finset },
-  obtain ⟨z, hz⟩ : ∃ z, z < m := exists_lt _,
-  exact hm₂ z (lt_trans hz hm₁) hz
-end
+lemma Ico_infinite : (Ico a b).infinite := (Ioo_infinite h).mono Ioo_subset_Ico_self
+lemma Ico.infinite : infinite (Ico a b) := infinite_coe_iff.2 $ Ico_infinite h
 
-lemma Iic.infinite {b : α} : (Iic b).infinite :=
-Iio.infinite.mono Iio_subset_Iic_self
+lemma Ioc_infinite : (Ioc a b).infinite := (Ioo_infinite h).mono Ioo_subset_Ioc_self
+lemma Ioc.infinite : infinite (Ioc a b) := infinite_coe_iff.2 $ Ioc_infinite h
 
-end unbounded_below
+lemma Icc_infinite : (Icc a b).infinite := (Ioo_infinite h).mono Ioo_subset_Icc_self
+lemma Icc.infinite : infinite (Icc a b) := infinite_coe_iff.2 $ Icc_infinite h
 
-section unbounded_above
+end densely_ordered
 
-variables [no_max_order α]
+instance [no_min_order α] {a : α} : infinite (Iio a) := no_min_order.infinite
+lemma Iio_infinite [no_min_order α] (a : α) : (Iio a).infinite := infinite_coe_iff.1 Iio.infinite
 
-lemma Ioi.infinite {a : α} : (Ioi a).infinite := @Iio.infinite αᵒᵈ _ _ _
+instance [no_min_order α] {a : α} : infinite (Iic a) := no_min_order.infinite
+lemma Iic_infinite [no_min_order α] (a : α) : (Iic a).infinite := infinite_coe_iff.1 Iic.infinite
 
-lemma Ici.infinite {a : α} : (Ici a).infinite :=
-Ioi.infinite.mono Ioi_subset_Ici_self
+instance [no_max_order α] {a : α} : infinite (Ioi a) := no_max_order.infinite
+lemma Ioi_infinite [no_min_order α] (a : α) : (Iio a).infinite := infinite_coe_iff.1 Iio.infinite
 
-end unbounded_above
+instance [no_max_order α] {a : α} : infinite (Ici a) := no_max_order.infinite
+lemma Ici_infinite [no_max_order α] (a : α) : (Ici a).infinite := infinite_coe_iff.1 Ici.infinite
 
 end set

src/order/lattice_intervals.lean

@@ -96,9 +96,6 @@ instance [preorder α] [order_bot α] : order_bot (Iic a) :=
 
 @[simp] lemma coe_bot [preorder α] [order_bot α] {a : α} : ↑(⊥ : Iic a) = (⊥ : α) := rfl
 
-instance [partial_order α] [no_min_order α] {a : α} : no_min_order (Iic a) :=
-⟨λ x, let ⟨y, hy⟩ := exists_lt x.1 in ⟨⟨y, le_trans hy.le x.2⟩, hy⟩ ⟩
-
 instance [preorder α] [order_bot α] : bounded_order (Iic a) :=
 { .. Iic.order_top,
   .. Iic.order_bot }
@@ -131,9 +128,6 @@ instance [preorder α] [order_top α] : order_top (Ici a) :=
 
 @[simp] lemma coe_top [preorder α] [order_top α] {a : α} : ↑(⊤ : Ici a) = (⊤ : α) := rfl
 
-instance [partial_order α] [no_max_order α] {a : α} : no_max_order (Ici a) :=
-⟨λ x, let ⟨y, hy⟩ := exists_gt x.1 in ⟨⟨y, le_trans x.2 hy.le⟩, hy⟩ ⟩
-
 instance [preorder α] [order_top α] : bounded_order (Ici a) :=
 { .. Ici.order_top,
   .. Ici.order_bot }

src/order/monotone.lean

@@ -646,6 +646,36 @@ nat.rel_of_forall_rel_succ_of_lt (<) hf
 lemma strict_anti_nat_of_succ_lt {f : ℕ → α} (hf : ∀ n, f (n + 1) < f n) : strict_anti f :=
 @strict_mono_nat_of_lt_succ αᵒᵈ _ f hf
 
+namespace nat
+
+/-- If `α` is a preorder with no maximal elements, then there exists a strictly monotone function
+`ℕ → α` with any prescribed value of `f 0`. -/
+lemma exists_strict_mono' [no_max_order α] (a : α) : ∃ f : ℕ → α, strict_mono f ∧ f 0 = a :=
+begin
+  have := (λ x : α, exists_gt x),
+  choose g hg,
+  exact ⟨λ n, nat.rec_on n a (λ _, g), strict_mono_nat_of_lt_succ $ λ n, hg _, rfl⟩
+end
+
+/-- If `α` is a preorder with no maximal elements, then there exists a strictly antitone function
+`ℕ → α` with any prescribed value of `f 0`. -/
+lemma exists_strict_anti' [no_min_order α] (a : α) : ∃ f : ℕ → α, strict_anti f ∧ f 0 = a :=
+exists_strict_mono' (order_dual.to_dual a)
+
+variable (α)
+
+/-- If `α` is a nonempty preorder with no maximal elements, then there exists a strictly monotone
+function `ℕ → α`. -/
+lemma exists_strict_mono [nonempty α] [no_max_order α] : ∃ f : ℕ → α, strict_mono f :=
+let ⟨a⟩ := ‹nonempty α›, ⟨f, hf, hfa⟩ := exists_strict_mono' a in ⟨f, hf⟩
+
+/-- If `α` is a nonempty preorder with no minimal elements, then there exists a strictly antitone
+function `ℕ → α`. -/
+lemma exists_strict_anti [nonempty α] [no_min_order α] : ∃ f : ℕ → α, strict_anti f :=
+exists_strict_mono αᵒᵈ
+
+end nat
+
 lemma int.rel_of_forall_rel_succ_of_lt (r : β → β → Prop) [is_trans β r]
   {f : ℤ → β} (h : ∀ n, r (f n) (f (n + 1))) ⦃a b : ℤ⦄ (hab : a < b) : r (f a) (f b) :=
 begin
@@ -672,6 +702,32 @@ int.rel_of_forall_rel_succ_of_lt (<) hf
 lemma strict_anti_int_of_succ_lt {f : ℤ → α} (hf : ∀ n, f (n + 1) < f n) : strict_anti f :=
 int.rel_of_forall_rel_succ_of_lt (>) hf
 
+namespace int
+
+variables (α) [nonempty α] [no_min_order α] [no_max_order α]
+
+/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
+monotone function `f : ℤ → α`. -/
+lemma exists_strict_mono : ∃ f : ℤ → α, strict_mono f :=
+begin
+  inhabit α,
+  rcases nat.exists_strict_mono' (default : α) with ⟨f, hf, hf₀⟩,
+  rcases nat.exists_strict_anti' (default : α) with ⟨g, hg, hg₀⟩,
+  refine ⟨λ n, int.cases_on n f (λ n, g (n + 1)), strict_mono_int_of_lt_succ _⟩,
+  rintro (n|_|n),
+  { exact hf n.lt_succ_self },
+  { show g 1 < f 0,
+    rw [hf₀, ← hg₀],
+    exact hg nat.zero_lt_one },
+  { exact hg (nat.lt_succ_self _) }
+end
+
+/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
+antitone function `f : ℤ → α`. -/
+lemma exists_strict_anti : ∃ f : ℤ → α, strict_anti f := exists_strict_mono αᵒᵈ
+
+end int
+
 -- TODO@Yael: Generalize the following four to succ orders
 /-- If `f` is a monotone function from `ℕ` to a preorder such that `x` lies between `f n` and
   `f (n + 1)`, then `x` doesn't lie in the range of `f`. -/