English
For a Finset s of indices and f: index → Ideal R, if i ∈ s and all f(y).radical = f(i).radical for y ∈ s, then (s.inf f).radical = f(i).radical.
Русский
Для конечного множества s индексов и функции f: индекс → Ideal R, если i ∈ s и для всех y ∈ s выполняется (f(y)).radical = (f(i)).radical, то (s.inf f).radical = (f(i)).radical.
LaTeX
$$$i \\in s \\Rightarrow (\\forall y \\in s, f(y).radical = f(i).radical) \\Rightarrow (s.inf f).radical = f(i).radical$$$
Lean4
theorem radical_finset_inf {ι} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s)
(hs : ∀ ⦃y⦄, y ∈ s → (f y).radical = (f i).radical) : (s.inf f).radical = (f i).radical :=
by
rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]
exact Finset.inf'_eq_of_forall _ _ hs
