span_prod_le — Mathlib

English

For s ⊆ R and t ⊆ S, span(s × t) ⊆ prod(span s, span t).

Русский

Для подмножеств s ⊆ R и t ⊆ S справедливо span(s × t) ⊆ prod(span s, span t).

LaTeX

$$$\\operatorname{span}(s) \\text{ and } \\operatorname{span}(t) \\implies \\operatorname{span}(s \\times t) \\le \\operatorname{prod}(\\operatorname{span}(s), \\operatorname{span}(t))$$$

Lean4

theorem span_prod_le {s : Set R} {t : Set S} : span (s ×ˢ t) ≤ prod (span s) (span t) :=
  by
  rw [ideal_prod_eq (span (s ×ˢ t)), map_span, map_span]
  gcongr
  · exact Set.fst_image_prod_subset _ _
  · exact Set.snd_image_prod_subset _ _

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