English
For a prime ideal I and a multiset s of real numbers, s.prod ∈ I iff there exists p ∈ s with p ∈ I.
Русский
Для простого идеала I и мультимножества s: произведение элементов s принадлежит I тогда существует p ∈ s, p ∈ I.
LaTeX
$$$ I.IsPrime → (s.prod \in I) \iff \exists p \in s, p \in I$$$
Lean4
/-- Another version of prime avoidance using `Set.Finite` instead of `Finset`. -/
theorem subset_union_prime_finite {R ι : Type*} [CommRing R] {s : Set ι} (hs : s.Finite) {f : ι → Ideal R} (a b : ι)
(hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime) {I : Ideal R} : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ∃ i ∈ s, I ≤ f i :=
by
rcases Set.Finite.exists_finset hs with ⟨t, ht⟩
have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
ext
simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)
have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) := (congrArg _ heq).to_iff
rw [hmem_union, Ideal.subset_union_prime a b (fun i hin ↦ hp i ((ht i).mp hin))]
exact exists_congr (fun i ↦ and_congr_left fun _ ↦ ht i)
