stableUnderGeneralization_singleton

English

For a point x in the prime spectrum, the singleton {x} is stable under generalization if and only if x.asIdeal is a minimal prime.

Русский

Для точки x в спектре простых идеалов множество {x} стабильно по обобщению тогда и только тогда, когда x.asIdeal является минимальным приматом.

LaTeX

$$$$ \operatorname{StableUnderGeneralization}(\{x\}) \iff x.\operatorname{asIdeal} \in \operatorname{minimalPrimes}(R). $$$$

Lean4

theorem stableUnderGeneralization_singleton {x : PrimeSpectrum R} :
    StableUnderGeneralization { x } ↔ x.asIdeal ∈ minimalPrimes R :=
  by
  simp_rw [← isMin_iff, StableUnderGeneralization, ← le_iff_specializes, Set.mem_singleton_iff, @forall_comm _ (_ = _),
    forall_eq]
  exact ⟨fun H a h ↦ (H a h).ge, fun H a h ↦ le_antisymm h (H h)⟩

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