mem_prod — Mathlib

English

Membership in the product subsemiring is equivalent to membership in each component: p ∈ s.prod t iff p.1 ∈ s ∧ p.2 ∈ t.

Русский

Членство в s.prod t эквивалентно членству в каждой компоненте: p ∈ s.prod t iff p.1 ∈ s ∧ p.2 ∈ t.

LaTeX

$$$ p \\in s.prod t \\iff p.1 \\in s \\wedge p.2 \\in t $$$

Lean4

theorem mem_prod {s : NonUnitalSubsemiring R} {t : NonUnitalSubsemiring S} {p : R × S} :
    p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t :=
  Iff.rfl

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