English
For an additive group G, the ray {x ∈ G : g ≤ x} is well-founded under < if and only if G is discrete (i.e., there exists an order isomorphism to ℤ).
Русский
Для аддитивной группы G множество {x ∈ G : g ≤ x} упорядочено по < и имеет хорошо упорядоченность тогда и только тогда, когда G дискретна (существует упорядочимое изоморфление с ℤ).
LaTeX
$$$\text{WellFoundedOn} \{x \in G : g \le x\} (<) \iff \exists \phi: G \cong_o \mathbb{Z}$$$
Lean4
theorem wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type*} [AddCommGroup G] [LinearOrder G]
[IsOrderedAddMonoid G] [Nontrivial G] {g : G} : Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ) :=
by
suffices Set.WellFoundedOn {x : G | 0 ≤ x} (· < ·) ↔ Nonempty (G ≃+o ℤ)
by
rw [← this]
refine ⟨fun h ↦ (h.mapsTo (· + g) ?_).mono' ?_, fun h ↦ (h.mapsTo (· - g) ?_).mono' ?_⟩ <;>
· try intro
simp [Function.onFun]
constructor
· intro h
replace h : WellFounded (α := {x : G | 0 ≤ x}) (· < ·) := h
rw [WellFounded.wellFounded_iff_has_min] at h
by_cases H : ∀ (x : G) {y}, 0 < y → ∃ n : ℕ, x ≤ n • y
· replace H : Archimedean G := ⟨H⟩
rw [LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered]
intro hd
obtain ⟨y, hy⟩ := exists_ne (0 : G)
wlog hy' : 0 < y generalizing y
· refine this (-y) ?_ ?_
· simp [hy]
· simp only [not_lt] at hy'
simp [lt_of_le_of_ne hy' hy]
obtain ⟨⟨z, hz⟩, hz', hz''⟩ := h ({x | ⟨0, le_rfl⟩ < x}) ⟨⟨y, hy'.le⟩, hy'⟩
obtain ⟨w, hw, hw'⟩ := exists_between hz'
exact hz'' ⟨w, hw.le⟩ hw hw'
· push_neg at H
exfalso
obtain ⟨x, y, hy0, H⟩ := H
obtain ⟨_, ⟨n, rfl⟩, hz⟩ := h (Set.range (fun n : ℕ ↦ ⟨x - n • y, sub_nonneg.mpr (H _).le⟩)) (range_nonempty _)
refine hz ⟨x - (n + 1) • y, sub_nonneg.mpr (H _).le⟩ ⟨_, rfl⟩ ?_
simp [add_smul, hy0]
· rintro ⟨f⟩
have : LocallyFiniteOrder G := LocallyFiniteOrder.ofOrderIsoClass f
exact BddBelow.wellFoundedOn_lt ⟨0, by simp [mem_lowerBounds]⟩
