mul_eq_span_mul_set — Mathlib

English

If x lies in span R (S · S'), then there exist finite sets T ⊆ S and T' ⊆ S' with x ∈ span R (T · T').

Русский

Если x ∈ span R (S·S'), то найдутся конечные множества T ⊆ S и T' ⊆ S', такие что x ∈ span R (T·T').

LaTeX

$$$x \\in \\operatorname{span}(R, S S') \\Rightarrow \\exists T,T'\\; (T \\subseteq S)\\land (T' \\subseteq S')\\land x \\in \\operatorname{span}(R, T T')$$$

Lean4

theorem mul_eq_span_mul_set (s t : Submodule R A) : s * t = span R ((s : Set A) * (t : Set A)) := by rw [mul_eq_map₂];
  exact map₂_eq_span_image2 _ s t

Похожие утверждения