mem_span_mul_finite_of_mem_mul — Mathlib

English

If x ∈ P·Q for submodules P,Q, then there exist finite T ⊆ P and T' ⊆ Q with x ∈ span(T · T').

Русский

Если x ∈ P·Q, то существуют конечные T ⊆ P и T' ⊆ Q, такие что x ∈ span(T·T').

LaTeX

$$$x \\in P \\cdot Q \\Rightarrow \\exists T,T' : Finset A, (T \\subseteq P) \\land (T' \\subseteq Q) \\land x \\in \\operatorname{span}(R, T T')$$$

Lean4

theorem mem_span_mul_finite_of_mem_mul {P Q : Submodule R A} {x : A} (hx : x ∈ P * Q) :
    ∃ T T' : Finset A, (T : Set A) ⊆ P ∧ (T' : Set A) ⊆ Q ∧ x ∈ span R (T * T' : Set A) :=
  Submodule.mem_span_mul_finite_of_mem_span_mul
    (by rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx)

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