English
Let S and T be subsets of a nonunital nonassociative semiring R. Then the product of their closures equals the closure of their set-theoretic product: closure(S) · closure(T) = closure(S · T).
Русский
Пусть S и T — подмножества кольца R без единицы и без ассоциативности относительно умножения. Тогда произведение их замыканий равно замыканию множества произведений: closure(S) · closure(T) = closure(S · T).
LaTeX
$$$\operatorname{closure}(S) \cdot \operatorname{closure}(T) = \operatorname{closure}(S \cdot T)$$$
Lean4
theorem closure_mul_closure (S T : Set R) : closure S * closure T = closure (S * T) :=
by
apply le_antisymm
· refine mul_le.2 fun a ha b hb => ?_
rw [← AddMonoidHom.mulRight_apply, ← AddSubmonoid.mem_comap]
refine (closure_le.2 fun a' ha' => ?_) ha
change b ∈ (closure (S * T)).comap (AddMonoidHom.mulLeft a')
refine (closure_le.2 fun b' hb' => ?_) hb
change a' * b' ∈ closure (S * T)
exact subset_closure (Set.mul_mem_mul ha' hb')
· rw [closure_le]
rintro _ ⟨a, ha, b, hb, rfl⟩
exact mul_mem_mul (subset_closure ha) (subset_closure hb)
