English
Under suitable archimedean hypotheses, there exists a least element b in the set {g ∈ H : 1 < g} for a nontrivial subgroup H.
Русский
При некоторых условиях архимедовости существует наименьший элемент b в множестве { g ∈ H | 1 < g } для не тривиальной подгруппы H.
LaTeX
$$$ \exists b \ IsLeast\\{ g \in H : 1 < g \} \\text{ в соответствующем контексте}. $$$
Lean4
/-- If a nontrivial subgroup of a linear ordered commutative group is disjoint
with the interval `Set.Ioo 1 a` for some `1 < a`, then the set of elements greater than 1 of this
group admits the least element. -/
@[to_additive /-- 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 exists_isLeast_one_lt {H : Subgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 1 < a)
(hd : Disjoint (H : Set G) (Ioo 1 a)) : ∃ b, IsLeast {g : G | g ∈ H ∧ 1 < g} b := by
-- todo: move to a lemma?
have hex : ∀ g > 1, ∃ n : ℕ, g ∈ Ioc (a ^ n) (a ^ (n + 1)) := fun g hg =>
by
rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩
simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'
lift m to ℕ
· rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
exact hg.trans_le hm
· simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
exact ⟨m, hm', hm⟩
have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (a ^ n) (a ^ (n + 1))) :=
by
rcases (bot_or_exists_ne_one H).resolve_left hbot with ⟨g, hgH, hg₀⟩
rcases hex |g|ₘ (one_lt_mabs.2 hg₀) with ⟨n, hn⟩
exact ⟨n, _, (@mabs_mem_iff (Subgroup 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, (one_le_pow_of_one_le' h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩
rcases hex y hy₀ with ⟨m, hm⟩
rcases lt_or_ge m n with hmn | hnm
· exact hmin m hmn ⟨y, hyH, hm⟩
· refine disjoint_left.1 hd (div_mem hxH hyH) ⟨one_lt_div'.2 hxy, div_lt_iff_lt_mul'.2 ?_⟩
calc
x ≤ a ^ (n + 1) := hxn
_ ≤ a ^ (m + 1) := (pow_le_pow_right' h₀.le (add_le_add_right hnm _))
_ = a ^ m * a := (pow_succ _ _)
_ < y * a := mul_lt_mul_right' hm.1 _
