English
For submonoids s ⊆ M, t ⊆ N and u ⊆ M × N, we have u ≤ s.prod t if and only if u.map (fst) ≤ s and u.map (snd) ≤ t.
Русский
Для подмоноидов s ⊆ M, t ⊆ N и u ⊆ M × N выполнено: u ≤ s.prod t тогда и только тогда, когда u.map fst ≤ s и u.map snd ≤ t.
LaTeX
$$$$ u \\le s.{prod} t \\;\\iff\\; u.{map}(\\mathrm{fst}) \\le s \\;\\wedge\\; u.{map}(\\mathrm{snd}) \\le t $$$$
Lean4
@[to_additive le_prod_iff]
theorem le_prod_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
u ≤ s.prod t ↔ u.map (fst M N) ≤ s ∧ u.map (snd M N) ≤ t :=
by
constructor
· intro h
constructor
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
exact (h hy1).1
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
exact (h hy1).2
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩
