finite_setOf_absNorm_le₀ — Mathlib

English

For CharZero S and any n, the set { I ∈ Ideal(S) | absNorm(I) ≤ n } is finite.

Русский

Для CharZero(S) и любого n множество { I ∈ Ideal(S) | absNorm(I) ≤ n } конечно.

LaTeX

$$$$\forall n\in \mathbb{N},\; \{ I\in \mathrm{Ideal}(S) \mid \operatorname{absNorm}(I) \le n\} \text{finite}. $$$$

Lean4

theorem finite_setOf_absNorm_le₀ [CharZero S] (n : ℕ) : {I : (Ideal S)⁰ | Ideal.absNorm (I : Ideal S) ≤ n}.Finite :=
  by
  have : Finite { I : Ideal S // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } := (finite_setOf_absNorm_le n).subset fun _ ⟨_, h⟩ ↦ h
  exact Finite.of_equiv _ (Equiv.subtypeSubtypeEquivSubtypeInter _ (fun I ↦ absNorm I ≤ n)).symm

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