isMin_iff — Mathlib

English

Alternate formulation: IsMin x is equivalent to x.asIdeal ∈ minimalPrimes R (same content in different form).

Русский

Альтернативная формулировка: IsMin x эквивалентно x.asIdeal ∈ minimalPrimes R (то же содержание в другой форме).

LaTeX

$$$IsMin\\ x \\iff x.asIdeal \\in minimalPrimes(R).$$$

Lean4

theorem isMin_iff {x : PrimeSpectrum R} : IsMin x ↔ x.asIdeal ∈ minimalPrimes R :=
  by
  change IsMin _ ↔ Minimal (fun q : Ideal R ↦ q.IsPrime ∧ ⊥ ≤ q) _
  simp only [IsMin, Minimal, x.2, bot_le, and_self, and_true, true_and]
  exact ⟨fun H y hy e ↦ @H ⟨y, hy⟩ e, fun H y e ↦ H y.2 e⟩

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