feat(data/set/finite): Add lemmas relating definitions of infinite sets (#18620)

dignissimus · YaelDillies · eric-wieser · dignissimus · commit 52fa514ec337 · 2023-04-25T23:03:08.000Z
Prove the following lemmas (and their dual)
* `set.infinite_of_forall_exists_lt`: `(∀ a, ∃ b ∈ s, a &lt; b) → s.infinite` in a nonempty preorder
* `set.infinite_iff_exists_lt`: `(∀ a, ∃ b ∈ s, a &lt; b) ↔ s.infinite` in a locally finite order with a bottom element



Co-authored-by: Yaël Dillies &lt;yael.dillies@gmail.com&gt;
Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean
@@ -259,6 +259,9 @@ lemma Ioi_subset_Ici_self : Ioi a ⊆ Ici a := by simpa [←coe_subset] using se
 lemma _root_.bdd_below.finite {s : set α} (hs : bdd_below s) : s.finite :=
 let ⟨a, ha⟩ := hs in (Ici a).finite_to_set.subset $ λ x hx, mem_Ici.2 $ ha hx
 
+lemma _root_.set.infinite.not_bdd_below {s : set α} : s.infinite → ¬ bdd_below s :=
+mt bdd_below.finite
+
 variables [fintype α]
 
 lemma filter_lt_eq_Ioi [decidable_pred ((<) a)] : univ.filter ((<) a) = Ioi a := by { ext, simp }
@@ -273,6 +276,9 @@ lemma Iio_subset_Iic_self : Iio a ⊆ Iic a := by simpa [←coe_subset] using se
 
 lemma _root_.bdd_above.finite {s : set α} (hs : bdd_above s) : s.finite := hs.dual.finite
 
+lemma _root_.set.infinite.not_bdd_above {s : set α} : s.infinite → ¬ bdd_above s :=
+mt bdd_above.finite
+
 variables [fintype α]
 
 lemma filter_gt_eq_Iio [decidable_pred (< a)] : univ.filter (< a) = Iio a := by { ext, simp }
@@ -504,6 +510,28 @@ end
 
 end locally_finite_order
 
+section locally_finite_order_bot
+variables [locally_finite_order_bot α] {s : set α}
+
+lemma _root_.set.infinite.exists_gt (hs : s.infinite) : ∀ a, ∃ b ∈ s, a < b :=
+not_bdd_above_iff.1 hs.not_bdd_above
+
+lemma _root_.set.infinite_iff_exists_gt [nonempty α] : s.infinite ↔ ∀ a, ∃ b ∈ s, a < b :=
+⟨set.infinite.exists_gt, set.infinite_of_forall_exists_gt⟩
+
+end locally_finite_order_bot
+
+section locally_finite_order_top
+variables [locally_finite_order_top α] {s : set α}
+
+lemma _root_.set.infinite.exists_lt (hs : s.infinite) : ∀ a, ∃ b ∈ s, b < a :=
+not_bdd_below_iff.1 hs.not_bdd_below
+
+lemma _root_.set.infinite_iff_exists_lt [nonempty α] : s.infinite ↔ ∀ a, ∃ b ∈ s, b < a :=
+⟨set.infinite.exists_lt, set.infinite_of_forall_exists_lt⟩
+
+end locally_finite_order_top
+
 variables [fintype α] [locally_finite_order_top α] [locally_finite_order_bot α]
 
 lemma Ioi_disj_union_Iio (a : α) :
diff --git a/src/data/nat/lattice.lean b/src/data/nat/lattice.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Floris van Doorn, Gabriel Ebner, Yury Kudryashov
 -/
+import data.nat.interval
 import order.conditionally_complete_lattice.finset
 
 /-!
@@ -37,7 +38,7 @@ lemma Sup_def {s : set ℕ} (h : ∃n, ∀a∈s, a ≤ n) :
 dif_pos _
 
 lemma _root_.set.infinite.nat.Sup_eq_zero {s : set ℕ} (h : s.infinite) : Sup s = 0 :=
-dif_neg $ λ ⟨n, hn⟩, let ⟨k, hks, hk⟩ := h.exists_nat_lt n in (hn k hks).not_lt hk
+dif_neg $ λ ⟨n, hn⟩, let ⟨k, hks, hk⟩ := h.exists_gt n in (hn k hks).not_lt hk
 
 @[simp] lemma Inf_eq_zero {s : set ℕ} : Inf s = 0 ↔ 0 ∈ s ∨ s = ∅ :=
 begin
diff --git a/src/data/nat/nth.lean b/src/data/nat/nth.lean
@@ -294,7 +294,7 @@ begin
   suffices h : Inf {i : ℕ | p i ∧ n ≤ i} ∈ {i : ℕ | p i ∧ n ≤ i},
   { exact h.2 },
   apply Inf_mem,
-  obtain ⟨m, hp, hn⟩ := hp.exists_nat_lt n,
+  obtain ⟨m, hp, hn⟩ := hp.exists_gt n,
   exact ⟨m, hp, hn.le⟩
 end
 
diff --git a/src/data/set/finite.lean b/src/data/set/finite.lean
@@ -1054,9 +1054,6 @@ theorem infinite_of_injective_forall_mem [infinite α] {s : set β} {f : α →
   (hi : injective f) (hf : ∀ x : α, f x ∈ s) : s.infinite :=
 by { rw ←range_subset_iff at hf, exact (infinite_range_of_injective hi).mono hf }
 
-lemma infinite.exists_nat_lt {s : set ℕ} (hs : s.infinite) (n : ℕ) : ∃ m ∈ s, n < m :=
-let ⟨m, hm⟩ := (hs.diff $ set.finite_le_nat n).nonempty in ⟨m, by simpa using hm⟩
-
 lemma infinite.exists_not_mem_finset {s : set α} (hs : s.infinite) (f : finset α) :
   ∃ a ∈ s, a ∉ f :=
 let ⟨a, has, haf⟩ := (hs.diff (to_finite f)).nonempty
@@ -1076,6 +1073,23 @@ end
 
 /-! ### Order properties -/
 
+section preorder
+variables [preorder α] [nonempty α] {s : set α}
+
+lemma infinite_of_forall_exists_gt (h : ∀ a, ∃ b ∈ s, a < b) : s.infinite :=
+begin
+  inhabit α,
+  set f : ℕ → α := λ n, nat.rec_on n (h default).some (λ n a, (h a).some),
+  have hf : ∀ n, f n ∈ s := by rintro (_ | _); exact (h _).some_spec.some,
+  refine infinite_of_injective_forall_mem (strict_mono_nat_of_lt_succ $ λ n, _).injective hf,
+  exact (h _).some_spec.some_spec,
+end
+
+lemma infinite_of_forall_exists_lt (h : ∀ a, ∃ b ∈ s, b < a) : s.infinite :=
+@infinite_of_forall_exists_gt αᵒᵈ _ _ _ h
+
+end preorder
+
 lemma finite_is_top (α : Type*) [partial_order α] : {x : α | is_top x}.finite :=
 (subsingleton_is_top α).finite
 
diff --git a/src/group_theory/exponent.lean b/src/group_theory/exponent.lean
@@ -196,7 +196,7 @@ variable {G}
 begin
   refine ⟨λ he, _, λ he, _⟩,
   { by_contra h,
-    obtain ⟨m, ⟨t, rfl⟩, het⟩ := set.infinite.exists_nat_lt h (exponent G),
+    obtain ⟨m, ⟨t, rfl⟩, het⟩ := set.infinite.exists_gt h (exponent G),
     exact pow_ne_one_of_lt_order_of' he het (pow_exponent_eq_one t) },
   { lift (set.range order_of) to finset ℕ using he with t ht,
     have htpos : 0 < t.prod id,
