English
I.jacobson = I iff every element outside I lies outside some maximal ideal containing I.
Русский
I^{jacobson} = I тогда и только тогда, когда любой элемент вне I лежит вне некоторого максимального идеала, содержащего I.
LaTeX
$$$I^{jacobson} = I \iff \forall x \notin I, \exists \mathfrak m: \text{Ideal}(R), (I \le \mathfrak m \land \mathfrak m \text{ maximal}) \land x \notin \mathfrak m$$$
Lean4
/-- An ideal `I` equals its Jacobson radical if and only if every element outside `I`
also lies outside of a maximal ideal containing `I`. -/
theorem eq_jacobson_iff_notMem : I.jacobson = I ↔ ∀ x ∉ I, ∃ M : Ideal R, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M :=
by
constructor
· intro h x hx
rw [← h, Ideal.jacobson, mem_sInf] at hx
push_neg at hx
exact hx
· refine fun h => le_antisymm (fun x hx => ?_) le_jacobson
contrapose hx
rw [Ideal.jacobson, mem_sInf]
push_neg
exact h x hx
