English
If s and t have the same nonemptiness pattern, then span(s × t) equals prod(span s, span t).
Русский
Если множества s и t либо оба пустые, либо оба непустые, то span(s × t) = prod(span s, span t).
LaTeX
$$theorem span_prod {s : Set R} {t : Set S} (hst : s.Nonempty ↔ t.Nonempty) : span (s ×ˢ t) = prod (span s) (span t)$$
Lean4
theorem span_prod {s : Set R} {t : Set S} (hst : s.Nonempty ↔ t.Nonempty) : span (s ×ˢ t) = prod (span s) (span t) :=
by
simp_rw [iff_iff_and_or_not_and_not, Set.not_nonempty_iff_eq_empty] at hst
obtain ⟨hs, ht⟩ | ⟨rfl, rfl⟩ := hst
· conv_lhs => rw [Ideal.ideal_prod_eq (Ideal.span (s ×ˢ t))]
congr 1
· rw [Ideal.map_span]
simp [Set.fst_image_prod _ ht]
· rw [Ideal.map_span]
simp [Set.snd_image_prod hs]
· simp
