feat: port Topology.Instances.Real (#2633)

I generalized some lemmas from additive subgroups of the real numbers to additive subgroups of an archimedean additive group.

Author: urkud

Mathlib.lean

@@ -1295,6 +1295,7 @@ import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Inseparable
 import Mathlib.Topology.Instances.Int
 import Mathlib.Topology.Instances.Nat
+import Mathlib.Topology.Instances.Real
 import Mathlib.Topology.Instances.Sign
 import Mathlib.Topology.IsLocallyHomeomorph
 import Mathlib.Topology.List

Mathlib/Algebra/Periodic.lean

@@ -40,7 +40,7 @@ period, periodic, periodicity, antiperiodic
 
 variable {α β γ : Type _} {f g : α → β} {c c₁ c₂ x : α}
 
-open BigOperators
+open Set BigOperators
 
 namespace Function
 
@@ -285,35 +285,46 @@ theorem Periodic.int_mul_eq [Ring α] (h : Periodic f c) (n : ℤ) : f (n * c) =
 /-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
   `y ∈ Ico 0 c` such that `f x = f y`. -/
 theorem Periodic.exists_mem_Ico₀ [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x) : ∃ y ∈ Set.Ico 0 c, f x = f y :=
+    (hc : 0 < c) (x) : ∃ y ∈ Ico 0 c, f x = f y :=
   let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
   ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩
 #align function.periodic.exists_mem_Ico₀ Function.Periodic.exists_mem_Ico₀
 
 /-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
   `y ∈ Ico a (a + c)` such that `f x = f y`. -/
 theorem Periodic.exists_mem_Ico [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x a) : ∃ y ∈ Set.Ico a (a + c), f x = f y :=
+    (hc : 0 < c) (x a) : ∃ y ∈ Ico a (a + c), f x = f y :=
   let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
   ⟨x + n • c, H, (h.zsmul n x).symm⟩
 #align function.periodic.exists_mem_Ico Function.Periodic.exists_mem_Ico
 
 /-- If a function `f` is `periodic` with positive period `c`, then for all `x` there exists some
   `y ∈ Ioc a (a + c)` such that `f x = f y`. -/
 theorem Periodic.exists_mem_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (x a) : ∃ y ∈ Set.Ioc a (a + c), f x = f y :=
+    (hc : 0 < c) (x a) : ∃ y ∈ Ioc a (a + c), f x = f y :=
   let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
   ⟨x + n • c, H, (h.zsmul n x).symm⟩
 #align function.periodic.exists_mem_Ioc Function.Periodic.exists_mem_Ioc
 
 theorem Periodic.image_Ioc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
-    (hc : 0 < c) (a : α) : f '' Set.Ioc a (a + c) = Set.range f :=
-  (Set.image_subset_range _ _).antisymm <|
-    Set.range_subset_iff.2 fun x =>
-      let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
-      ⟨y, hy, hyx.symm⟩
+    (hc : 0 < c) (a : α) : f '' Ioc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <|range_subset_iff.2 fun x =>
+    let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
+    ⟨y, hy, hyx.symm⟩
 #align function.periodic.image_Ioc Function.Periodic.image_Ioc
 
+theorem Periodic.image_Icc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : 0 < c) (a : α) : f '' Icc a (a + c) = range f :=
+  (image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_subset _ Ioc_subset_Icc_self
+
+theorem Periodic.image_uIcc [LinearOrderedAddCommGroup α] [Archimedean α] (h : Periodic f c)
+    (hc : c ≠ 0) (a : α) : f '' uIcc a (a + c) = range f := by
+  cases hc.lt_or_lt with
+  | inl hc =>
+    rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
+      add_neg_cancel_right]
+  | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
+
 theorem periodic_with_period_zero [AddZeroClass α] (f : α → β) : Periodic f 0 := fun x => by
   rw [add_zero]
 #align function.periodic_with_period_zero Function.periodic_with_period_zero

Mathlib/GroupTheory/Archimedean.lean

@@ -34,11 +34,9 @@ The result is also used in `Topology.Instances.Real` as an ingredient in the cla
 subgroups of `ℝ`.
 -/
 
-
+open Set
 variable {G : Type _} [LinearOrderedAddCommGroup G] [Archimedean G]
 
-open LinearOrderedAddCommGroup
-
 /-- Given a subgroup `H` of a decidable linearly ordered archimedean abelian group `G`, if there
 exists a minimal element `a` of `H ∩ G_{>0}` then `H` is generated by `a`. -/
 theorem AddSubgroup.cyclic_of_min {H : AddSubgroup G} {a : G}
@@ -58,21 +56,49 @@ theorem AddSubgroup.cyclic_of_min {H : AddSubgroup G} {a : G}
   simp [sub_eq_zero.mp h_zero, AddSubgroup.mem_closure_singleton]
 #align add_subgroup.cyclic_of_min AddSubgroup.cyclic_of_min
 
+/-- If a nontrivial additive subgroup of a linear ordered additive commutative group is disjoint
+with the interval `Set.Ioo 0 a` for some positive `a`, then the set of positive elements of this
+group admits the least element. -/
+theorem AddSubgroup.exists_isLeast_pos {H : AddSubgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 0 < a)
+    (hd : Disjoint (H : Set G) (Ioo 0 a)) : ∃ b, IsLeast { g : G | g ∈ H ∧ 0 < g } b := by
+  -- todo: move to a lemma?
+  have hex : ∀ g > 0, ∃ n : ℕ, g ∈ Ioc (n • a) ((n + 1) • a) := fun g hg => by
+    rcases existsUnique_add_zsmul_mem_Ico h₀ 0 (g - a) with ⟨m, ⟨hm, hm'⟩, -⟩
+    simp only [zero_add, sub_le_iff_le_add, sub_add_cancel, ← add_one_zsmul] at hm hm'
+    lift m to ℕ
+    · rw [← Int.lt_add_one_iff, ← zsmul_lt_zsmul_iff h₀, zero_zsmul]
+      exact hg.trans_le hm
+    · simp only [← Nat.cast_succ, coe_nat_zsmul] at hm hm'
+      exact ⟨m, hm', hm⟩
+  have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (n • a) ((n + 1) • a))
+  · rcases (bot_or_exists_ne_zero H).resolve_left hbot with ⟨g, hgH, hg₀⟩
+    rcases hex (|g|) (abs_pos.2 hg₀) with ⟨n, hn⟩
+    exact ⟨n, _, (@abs_mem_iff (AddSubgroup G) G _ _).2 hgH, hn⟩
+  classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
+  by_contra hxmin
+  simp only [IsLeast, not_and, mem_setOf_eq, mem_lowerBounds, not_exists, not_forall,
+    not_le] at hxmin
+  rcases hxmin x ⟨hxH, (nsmul_nonneg h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩
+  rcases hex y hy₀ with ⟨m, hm⟩
+  cases' lt_or_le m n with hmn hnm
+  · exact hmin m hmn ⟨y, hyH, hm⟩
+  · refine disjoint_left.1 hd (sub_mem hxH hyH) ⟨sub_pos.2 hxy, sub_lt_iff_lt_add'.2 ?_⟩
+    calc x ≤ (n + 1) • a := hxn
+    _ ≤ (m + 1) • a := nsmul_le_nsmul h₀.le (add_le_add_right hnm _)
+    _ = m • a + a := succ_nsmul' _ _
+    _ < y + a := add_lt_add_right hm.1 _
+
+/-- If an additive subgroup of a linear ordered additive commutative group is disjoint with the
+interval `Set.Ioo 0 a` for some positive `a`, then this is a cyclic subgroup. -/
+theorem AddSubgroup.cyclic_of_isolated_zero {H : AddSubgroup G} {a : G} (h₀ : 0 < a)
+    (hd : Disjoint (H : Set G) (Ioo 0 a)) : ∃ b, H = closure {b} := by
+  rcases eq_or_ne H ⊥ with rfl | hbot
+  · exact ⟨0, closure_singleton_zero.symm⟩
+  · exact (exists_isLeast_pos hbot h₀ hd).imp fun _ => cyclic_of_min
+
 /-- Every subgroup of `ℤ` is cyclic. -/
-theorem Int.subgroup_cyclic (H : AddSubgroup ℤ) : ∃ a, H = AddSubgroup.closure {a} := by
-  cases' AddSubgroup.bot_or_exists_ne_zero H with h h
-  · use 0
-    rw [h]
-    exact AddSubgroup.closure_singleton_zero.symm
-  let s := { g : ℤ | g ∈ H ∧ 0 < g }
-  have h_bdd : ∀ g ∈ s, (0 : ℤ) ≤ g := fun _ h => le_of_lt h.2
-  obtain ⟨g₀, g₀_in, g₀_ne⟩ := h
-  obtain ⟨g₁, g₁_in, g₁_pos⟩ : ∃ g₁ : ℤ, g₁ ∈ H ∧ 0 < g₁ :=
-    by
-    cases' lt_or_gt_of_ne g₀_ne with Hg₀ Hg₀
-    · exact ⟨-g₀, H.neg_mem g₀_in, neg_pos.mpr Hg₀⟩
-    · exact ⟨g₀, g₀_in, Hg₀⟩
-  classical
-  obtain ⟨a, ha, ha'⟩ := Int.exists_least_of_bdd ⟨(0 : ℤ), h_bdd⟩ ⟨g₁, g₁_in, g₁_pos⟩
-  exact ⟨a, AddSubgroup.cyclic_of_min ⟨ha, ha'⟩⟩
+theorem Int.subgroup_cyclic (H : AddSubgroup ℤ) : ∃ a, H = AddSubgroup.closure {a} :=
+  have : Ioo (0 : ℤ) 1 = ∅ := eq_empty_of_forall_not_mem fun m hm =>
+    hm.1.not_le (lt_add_one_iff.1 hm.2) 
+  AddSubgroup.cyclic_of_isolated_zero one_pos <| by simp [this]
 #align int.subgroup_cyclic Int.subgroup_cyclic

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -134,6 +134,10 @@ theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G]
 #align inv_mem_iff inv_mem_iff
 #align neg_mem_iff neg_mem_iff
 
+@[simp] theorem abs_mem_iff {S G} [InvolutiveNeg G] [LinearOrder G] {_ : SetLike S G}
+    [NegMemClass S G] {H : S} {x : G} : |x| ∈ H ↔ x ∈ H := by
+  cases abs_choice x <;> simp [*]
+
 variable {M S : Type _} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}
 
 /-- A subgroup is closed under division. -/

Mathlib/Order/Filter/Cofinite.lean

@@ -59,6 +59,13 @@ instance cofinite_neBot [Infinite α] : NeBot (@cofinite α) :=
   hasBasis_cofinite.neBot_iff.2 fun hs => hs.infinite_compl.nonempty
 #align filter.cofinite_ne_bot Filter.cofinite_neBot
 
+@[simp]
+theorem cofinite_eq_bot_iff : @cofinite α = ⊥ ↔ Finite α := by
+  simp [← empty_mem_iff_bot, finite_univ_iff]
+
+@[simp]
+theorem cofinite_eq_bot [Finite α] : @cofinite α = ⊥ := cofinite_eq_bot_iff.2 ‹_›
+
 theorem frequently_cofinite_iff_infinite {p : α → Prop} :
     (∃ᶠ x in cofinite, p x) ↔ Set.Infinite { x | p x } := by
   simp only [Filter.Frequently, Filter.Eventually, mem_cofinite, compl_setOf, not_not,
@@ -182,6 +189,9 @@ theorem Filter.Tendsto.exists_forall_ge [Nonempty α] [LinearOrder β] {f : α 
   @Filter.Tendsto.exists_forall_le _ βᵒᵈ _ _ _ hf
 #align filter.tendsto.exists_forall_ge Filter.Tendsto.exists_forall_ge
 
+theorem Function.Surjective.le_map_cofinite {f : α → β} (hf : Surjective f) :
+    cofinite ≤ map f cofinite := fun _ h => .of_preimage h hf
+
 /-- For an injective function `f`, inverse images of finite sets are finite. See also
 `Filter.comap_cofinite_le` and `Function.Injective.comap_cofinite_eq`. -/
 theorem Function.Injective.tendsto_cofinite {f : α → β} (hf : Injective f) :

Mathlib/Topology/Algebra/Order/Archimedean.lean

@@ -9,21 +9,67 @@ Authors: Yury G. Kudryashov
 ! if you have ported upstream changes.
 -/
 import Mathlib.Topology.Order.Basic
-import Mathlib.Algebra.Order.Archimedean
+import Mathlib.GroupTheory.Archimedean
 
 /-!
-# Rational numbers are dense in a linear ordered archimedean field
+# Topology on archimedean groups and fields
 
-In this file we prove that coercion from `ℚ` to a linear ordered archimedean field has dense range.
-This lemma is in a separate file because `Mathlib.Topology.Order.Basic` does not import
-`Mathlib.Algebra.Order.Archimedean`.
--/
+In this file we prove the following theorems:
+
+- `Rat.denseRange_cast`: the coercion from `ℚ` to a linear ordered archimedean field has dense
+  range;
 
+- `AddSubgroup.dense_of_not_isolated_zero`, `AddSubgroup.dense_of_no_min`: two sufficient conditions
+  for a subgroup of an archimedean linear ordered additive commutative group to be dense;
+
+- `AddSubgroup.dense_or_cyclic`: an additive subgroup of an archimedean linear ordered additive
+  commutative group `G` with order topology either is dense in `G` or is a cyclic subgroup.
+-/
 
-variable {𝕜 : Type _} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [Archimedean 𝕜]
+open Set
 
 /-- Rational numbers are dense in a linear ordered archimedean field. -/
-theorem Rat.denseRange_cast : DenseRange ((↑) : ℚ → 𝕜) :=
+theorem Rat.denseRange_cast {𝕜} [LinearOrderedField 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+  [Archimedean 𝕜] : DenseRange ((↑) : ℚ → 𝕜) :=
   dense_of_exists_between fun _ _ h => Set.exists_range_iff.2 <| exists_rat_btwn h
 #align rat.dense_range_cast Rat.denseRange_cast
 
+namespace AddSubgroup
+
+variable {G : Type _} [LinearOrderedAddCommGroup G] [TopologicalSpace G] [OrderTopology G]
+  [Archimedean G]
+
+/-- An additive subgroup of an archimedean linear ordered additive commutative group with order
+topology is dense provided that for all positive `ε` there exists a positive element of the
+subgroup that is less than `ε`. -/
+theorem dense_of_not_isolated_zero (S : AddSubgroup G) (hS : ∀ ε > 0, ∃ g ∈ S, g ∈ Ioo 0 ε) :
+    Dense (S : Set G) := by
+  cases subsingleton_or_nontrivial G
+  · refine fun x => _root_.subset_closure ?_
+    rw [Subsingleton.elim x 0]
+    exact zero_mem S
+  refine dense_of_exists_between fun a b hlt => ?_
+  rcases hS (b - a) (sub_pos.2 hlt) with ⟨g, hgS, hg0, hg⟩
+  rcases (existsUnique_add_zsmul_mem_Ioc hg0 0 a).exists with ⟨m, hm⟩
+  rw [zero_add] at hm
+  refine ⟨m • g, zsmul_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
+  rwa [lt_sub_iff_add_lt'] at hg
+
+/-- Let `S` be a nontrivial additive subgroup in an archimedean linear ordered additive commutative
+group `G` with order topology. If the set of positive elements of `S` does not have a minimal
+element, then `S` is dense `G`. -/
+theorem dense_of_no_min (S : AddSubgroup G) (hbot : S ≠ ⊥)
+    (H : ¬∃ a : G, IsLeast { g : G | g ∈ S ∧ 0 < g } a) : Dense (S : Set G) := by
+  refine S.dense_of_not_isolated_zero fun ε ε0 => ?_
+  contrapose! H
+  exact exists_isLeast_pos hbot ε0 (disjoint_left.2 H)
+#align real.subgroup_dense_of_no_min AddSubgroup.dense_of_no_minₓ
+
+/-- An additive subgroup of an archimedean linear ordered additive commutative group `G` with order
+topology either is dense in `G` or is a cyclic subgroup. -/
+theorem dense_or_cyclic (S : AddSubgroup G) : Dense (S : Set G) ∨ ∃ a : G, S = closure {a} := by
+  refine (em _).imp (dense_of_not_isolated_zero S) fun h => ?_
+  push_neg at h
+  rcases h with ⟨ε, ε0, hε⟩
+  exact cyclic_of_isolated_zero ε0 (disjoint_left.2 hε)
+#align real.subgroup_dense_or_cyclic AddSubgroup.dense_or_cyclicₓ