feat(data/set/intervals/infinite): intervals are infinite (#4241)

src/data/fintype/basic.lean

@@ -1050,6 +1050,19 @@ class infinite (α : Type*) : Prop :=
 @[simp] lemma not_nonempty_fintype {α : Type*} : ¬nonempty (fintype α) ↔ infinite α :=
 ⟨λf, ⟨λ x, f ⟨x⟩⟩, λ⟨f⟩ ⟨x⟩, f x⟩
 
+lemma finset.exists_minimal {α : Type*} [preorder α] (s : finset α) (h : s.nonempty) :
+  ∃ m ∈ s, ∀ x ∈ s, ¬ (x < m) :=
+begin
+  obtain ⟨c, hcs : c ∈ s⟩ := h,
+  have : well_founded (@has_lt.lt {x // x ∈ s} _) := fintype.well_founded_of_trans_of_irrefl _,
+  obtain ⟨⟨m, hms : m ∈ s⟩, -, H⟩ := this.has_min set.univ ⟨⟨c, hcs⟩, trivial⟩,
+  exact ⟨m, hms, λ x hx hxm, H ⟨x, hx⟩ trivial hxm⟩,
+end
+
+lemma finset.exists_maximal {α : Type*} [preorder α] (s : finset α) (h : s.nonempty) :
+  ∃ m ∈ s, ∀ x ∈ s, ¬ (m < x) :=
+@finset.exists_minimal (order_dual α) _ s h
+
 namespace infinite
 
 lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=

src/data/set/finite.lean

@@ -39,6 +39,11 @@ noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
 @[simp] theorem finite.mem_to_finset {s : set α} {h : finite s} {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
 @mem_to_finset _ _ h.fintype _
 
+@[simp] theorem finite.to_finset.nonempty {s : set α} (h : finite s) :
+  h.to_finset.nonempty ↔ s.nonempty :=
+show (∃ x, x ∈ h.to_finset) ↔ (∃ x, x ∈ s),
+from exists_congr (λ _, finite.mem_to_finset)
+
 @[simp] lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
 @set.coe_to_finset _ s h.fintype
 
@@ -221,6 +226,9 @@ by rw ← inter_eq_self_of_subset_right h; apply_instance
 theorem finite.subset {s : set α} : finite s → ∀ {t : set α}, t ⊆ s → finite t
 | ⟨hs⟩ t h := ⟨@set.fintype_subset _ _ _ hs (classical.dec_pred t) h⟩
 
+theorem infinite_mono {s t : set α} (h : s ⊆ t) : infinite s → infinite t :=
+mt (λ ht, ht.subset h)
+
 instance fintype_image [decidable_eq β] (s : set α) (f : α → β) [fintype s] : fintype (f '' s) :=
 fintype.of_finset (s.to_finset.image f) $ by simp
 

src/data/set/intervals/infinite.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2020 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton
+-/
+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.
+-/
+
+namespace set
+
+variables {α : Type*} [preorder α]
+
+section bounded
+
+variables [densely_ordered α]
+
+lemma Ioo.infinite {a b : α} (h : a < b) : infinite (Ioo a b) :=
+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 := dense hm₁.1,
+  exact hm₂ z ⟨hz₁, lt_trans hz₂ hm₁.2⟩ hz₂,
+end
+
+lemma Ico.infinite {a b : α} (h : a < b) : infinite (Ico a b) :=
+infinite_mono Ioo_subset_Ico_self (Ioo.infinite h)
+
+lemma Ioc.infinite {a b : α} (h : a < b) : infinite (Ioc a b) :=
+infinite_mono Ioo_subset_Ioc_self (Ioo.infinite h)
+
+lemma Icc.infinite {a b : α} (h : a < b) : infinite (Icc a b) :=
+infinite_mono Ioo_subset_Icc_self (Ioo.infinite h)
+
+end bounded
+
+section unbounded_below
+
+variables [no_bot_order α]
+
+lemma Iio.infinite {b : α} : infinite (Iio b) :=
+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 := no_bot _,
+  exact hm₂ z (lt_trans hz hm₁) hz
+end
+
+lemma Iic.infinite {b : α} : infinite (Iic b) :=
+infinite_mono Iio_subset_Iic_self Iio.infinite
+
+end unbounded_below
+
+section unbounded_above
+
+variables [no_top_order α]
+
+lemma Ioi.infinite {a : α} : infinite (Ioi a) :=
+by apply @Iio.infinite (order_dual α)
+
+lemma Ici.infinite {a : α} : infinite (Ici a) :=
+infinite_mono Ioi_subset_Ici_self Ioi.infinite
+
+end unbounded_above
+
+end set