finite_setOf_addOrderOf_eq — Mathlib

English

Let p define the additive circle AddCircle(p). For every natural number n > 0, the set {u in AddCircle(p) | addOrderOf(u) = n} is finite.

Русский

Пусть p задаёт аддитивный круг AddCircle(p). Для каждого натурального n > 0 множество {u ∈ AddCircle(p) | addOrderOf(u) = n} конечно.

LaTeX

$$$$ \\#\\{ u \\in \\mathrm{AddCircle}(p) \\mid \\operatorname{addOrderOf}(u) = n \\} < \\infty $$$$

Lean4

theorem finite_setOf_addOrderOf_eq {n : ℕ} (hn : 0 < n) : {u : AddCircle p | addOrderOf u = n}.Finite :=
  finite_coe_iff.mp <| Nat.finite_of_card_ne_zero <| by simp [hn.ne']

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