wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete

English

In a linearly ordered multiplicative group, the ray {x | g ≤ x} is well-founded under < if and only if there is a multiplicative order isomorphism to ℤᵐ⁰.

Русский

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

LaTeX

$$$\text{WellFoundedOn} \{x : G \mid g \le x\} (<) \iff \exists \phi: G \cong_* o \mathbb{Z}^{\mathbf{m0}}$$$

Lean4

theorem wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete {G : Type*} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G]
    [Nontrivial G] (g : G) : Set.WellFoundedOn {x : G | x ≤ g} (· > ·) ↔ Nonempty (G ≃*o Multiplicative ℤ) :=
  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, inv_le']

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