range_asIdeal — Mathlib

English

The image of the map asIdeal from PrimeSpectrum R equals the set of prime ideals of R.

Русский

Образ отображения asIdeal из PrimeSpectrum(R) равен множеству простых идеалов кольца R.

LaTeX

$$$\\\\operatorname{range}(\\\\operatorname{PrimeSpectrum}.asIdeal) = {\\\\! J \\\\in \\\\operatorname{Ideal}(R) \\\\mid J.\\\\IsPrime}$$$

Lean4

theorem range_asIdeal : Set.range PrimeSpectrum.asIdeal = {J : Ideal R | J.IsPrime} :=
  Set.ext fun J ↦
    ⟨fun hJ ↦
      let ⟨j, hj⟩ := Set.mem_range.mp hJ;
      Set.mem_setOf.mpr <| hj ▸ j.isPrime,
      fun hJ ↦ Set.mem_range.mpr ⟨⟨J, Set.mem_setOf.mp hJ⟩, rfl⟩⟩

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