English
For x,y in R and Ideals I,J, span{x} · I = span{y} · J iff the two containment conditions hold: (i) every z_I ∈ I has a z_J ∈ J with x z_I = y z_J, and (ii) every z_J ∈ J has a z_I ∈ I with x z_I = y z_J.
Русский
Пусть x,y ∈ R и идеалы I,J. Тогда span{x} · I = span{y} · J тогда и только тогда, когда выполняются две условия: (i) для каждого z_I ∈ I существует z_J ∈ J с x z_I = y z_J, и (ii) для каждого z_J ∈ J существует z_I ∈ I с x z_I = y z_J.
LaTeX
$$$\operatorname{span}\{x\} \cdot I = \operatorname{span}\{y\} \cdot J \iff \Big(\forall z_I\in I,\exists z_J\in J, x z_I = y z_J\Big) \land \Big(\forall z_J\in J, \exists z_I\in I, x z_I = y z_J\Big)$$$
Lean4
theorem span_singleton_mul_eq_span_singleton_mul {x y : R} (I J : Ideal R) :
span { x } * I = span { y } * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ := by
simp only [le_antisymm_iff, span_singleton_mul_le_span_singleton_mul, eq_comm]
