English
Let S ⊆ M and T ⊆ N be subsemigroups, and U ⊆ M × N a subsemigroup. Then U ≤ S × T if and only if U.map fst ≤ S and U.map snd ≤ T; i.e., the projections of U lie in S and T respectively.
Русский
Пусть S ⊆ M и T ⊆ N — подполугруппы, а U ⊆ M × N — подполугруппа. Тогда U ≤ S × T тогда и только тогда, когда образ U под fst ≤ S и образ U под snd ≤ T; то есть проекции U принадлежат S и T соответственно.
LaTeX
$$$u \le s \times t \;\Longleftrightarrow\; u\mapsto \mathrm{fst} \;u \le s \ \wedge\; u\mapsto \mathrm{snd} \;u \le t$$$
Lean4
@[to_additive le_prod_iff]
theorem le_prod_iff {s : Subsemigroup M} {t : Subsemigroup N} {u : Subsemigroup (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⟩⟩
