wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete

English

In an additive linearly ordered group, the well-foundedness of the ray {x | g ≤ x} under < is equivalent to the existence of an order isomorphism to ℤ.

Русский

В аддитивной линейно упорядоченной группе хорошоупорядоченность луча {x | g ≤ x} по < эквивалентна существованию упорядочимого изоморфизма с ℤ.

LaTeX

$$$(\exists \phi: G \cong_o \mathbb{Z}) \iff \text{WellFoundedOn} \{x \in G : g \le x\} (<)$$$

Lean4

theorem wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type*} [AddCommGroup G] [LinearOrder G]
    [IsOrderedAddMonoid G] [Nontrivial G] (g : G) : Set.WellFoundedOn {x : G | x ≤ g} (· > ·) ↔ Nonempty (G ≃+o ℤ) :=
  by
  rw [← wellFoundedOn_setOf_le_lt_iff_nonempty_discrete (g := -g)]
  refine ⟨fun h ↦ (h.mapsTo (-·) ?_).mono' ?_, fun h ↦ (h.mapsTo (-·) ?_).mono' ?_⟩ <;>
    · intro
      simp [Function.onFun, neg_le]

Похожие утверждения