infinite_not_isOfFinOrder — Mathlib

English

If x has infinite order, the set of elements not of finite order is infinite.

Русский

Если порядок x бесконечен, множество элементов не имеющих конечного порядка бесконечно.

LaTeX

$$({x : G} \ operatorname{IsOfFinOrder}(x))^c \text{ implies } {y : G | ¬IsOfFinOrder(y)}.Infinite$$

Lean4

@[to_additive]
theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) : {y : G | ¬IsOfFinOrder y}.Infinite :=
  by
  let s := {n | 0 < n}.image fun n : ℕ => x ^ n
  have hs : s ⊆ {y : G | ¬IsOfFinOrder y} :=
    by
    rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
    apply h
    rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
    obtain ⟨m, hm, hm'⟩ := contra
    exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
  suffices s.Infinite by exact this.mono hs
  contrapose! h
  have : ¬Injective fun n : ℕ => x ^ n :=
    by
    have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
    contrapose! this
    exact Set.injOn_of_injective this
  rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

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