English
Any set of pairs s ⊆ α × β is contained in the product of its projections.
Русский
Любое множество пар s ⊆ α × β содержится в произведении его проекций.
LaTeX
$$$ s \subseteq (\mathrm{fst}'' s) \times (\mathrm{snd}'' s) $$$
Lean4
/-- A product set is included in a product set if and only factors are included, or a factor of the
first set is empty. -/
theorem prod_subset_prod_iff : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅ :=
by
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
· simp [h, prod_eq_empty_iff.1 h]
have st : s.Nonempty ∧ t.Nonempty := by rwa [prod_nonempty_iff] at h
refine ⟨fun H => Or.inl ⟨?_, ?_⟩, ?_⟩
· have := image_mono (f := Prod.fst) H
rwa [fst_image_prod _ st.2, fst_image_prod _ (h.mono H).snd] at this
· have := image_mono (f := Prod.snd) H
rwa [snd_image_prod st.1, snd_image_prod (h.mono H).fst] at this
· intro H
simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
exact prod_mono H.1 H.2
