mem_prod — Mathlib

English

Membership in the product subsemigroup S.prod T is equivalent to membership in S for the first coordinate and in T for the second.

Русский

Членство в S.prod T эквивалентно членству в S по первой координате и в T по второй.

LaTeX

$$p ∈ S.prod T ↔ p.1 ∈ S ∧ p.2 ∈ T$$

Lean4

@[to_additive mem_prod]
theorem mem_prod {s : Subsemigroup M} {t : Subsemigroup N} {p : M × N} : p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Iff.rfl

Похожие утверждения