wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero

English

For a nontrivial linearly ordered group with zero, there is an equivalence between discreteness and not being densely ordered (via a zero-extended structure).

Русский

Для не тривиальной линейно упорядоченной группы с нулем существует эквивалентность между дискретностью и тем, что упорядочение не плотное (через структуру с нулем).

LaTeX

$$$(\exists \phi: G \cong_* o \mathbb{Z}^{\mathbf{m0}}) \iff \lnot \mathrm{DenselyOrdered}(G)$$$

Lean4

theorem wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀]
    [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) : Set.WellFoundedOn {x : G₀ | g ≤ x} (· < ·) ↔ Nonempty (G₀ ≃*o ℤᵐ⁰) :=
  by
  suffices Set.WellFoundedOn {x : G₀ | g ≤ x} (· < ·) ↔ Set.WellFoundedOn {x : G₀ˣ | Units.mk0 g hg ≤ x} (· < ·)
    by
    rw [this, LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete]
    refine Nonempty.congr (fun f ↦ ⟨?_, ?_⟩) (fun f ↦ ⟨?_, ?_⟩)
    · exact WithZero.withZeroUnitsEquiv.symm.trans f.withZero
    · intro a b
      rcases eq_or_ne a 0 with rfl | ha
      · simp [WithZero.withZeroUnitsEquiv]
      rcases eq_or_ne b 0 with rfl | hb
      · simp [WithZero.withZeroUnitsEquiv]
      simp [WithZero.withZeroUnitsEquiv, ha, hb, ← Units.val_le_val]
    · exact MulEquiv.withZero.symm (WithZero.withZeroUnitsEquiv.trans f)
    · intros
      rw [← WithZero.coe_le_coe]
      simp
  rw [← Set.wellFoundedOn_sdiff_singleton (a := 0)]
  refine ⟨fun h ↦ (h.mapsTo Units.val ?_).mono' ?_, fun h ↦ (h.mapsTo ?_ ?_).mono' ?_⟩
  · intro
    simp [← Units.val_le_val]
  · simp [Function.onFun]
  · exact fun x ↦ if h : x = 0 then 1 else Units.mk0 x h
  · simp +contextual [← Units.val_le_val, MapsTo]
  · simp only [mem_diff, mem_setOf_eq, mem_singleton_iff, Function.onFun, and_imp]
    intro _ _ ha0 _ _ hb0 h
    simp [ha0, hb0, ← Units.val_lt_val, h]

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