finite_setOf_isMin — Mathlib

English

For Noetherian R, the set {x ∈ Spec(R) | IsMin x} is finite.

Русский

Для Noetherian R множество {x ∈ Spec(R) | IsMin x} конечное.

LaTeX

$$$\\{x \\in \\mathrm{PrimeSpectrum}(R) \\mid \\mathrm{IsMin}(x)\\}.\\Finite$$$

Lean4

theorem finite_setOf_isMin : {x : PrimeSpectrum R | IsMin x}.Finite :=
  by
  have : Function.Injective (asIdeal (R := R)) := @PrimeSpectrum.ext _ _
  refine Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn
  simp_rw [isMin_iff]
  exact (minimalPrimes.finite_of_isNoetherianRing R).subset (Set.image_preimage_subset _ _)

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