English
For submonoids s ⊆ M, t ⊆ N and u ⊆ M × N, s.prod t ≤ u if and only if s.map (fst) ≤ u and t.map (snd) ≤ u.
Русский
Для подмонойдов s ⊆ M, t ⊆ N и u ⊆ M × N верно: s.prod t ≤ u тогда и только тогда, когда s.map fst ≤ u и t.map snd ≤ u.
LaTeX
$$$$ s.{prod}t \\le u \\;\\iff\\; s.{map}(\\mathrm{fst}) \\le u \\;\\wedge\\; t.{map}(\\mathrm{snd}) \\le u $$$$
Lean4
@[to_additive prod_le_iff]
theorem prod_le_iff {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} :
s.prod t ≤ u ↔ s.map (inl M N) ≤ u ∧ t.map (inr M N) ≤ u :=
by
constructor
· intro h
constructor
· rintro _ ⟨x, hx, rfl⟩
apply h
exact ⟨hx, Submonoid.one_mem _⟩
· rintro _ ⟨x, hx, rfl⟩
apply h
exact ⟨Submonoid.one_mem _, hx⟩
· rintro ⟨hH, hK⟩ ⟨x1, x2⟩ ⟨h1, h2⟩
have h1' : inl M N x1 ∈ u := by
apply hH
simpa using h1
have h2' : inr M N x2 ∈ u := by
apply hK
simpa using h2
simpa using Submonoid.mul_mem _ h1' h2'
