mem_prod — Mathlib

English

An element of the product belongs to prod S S₁ iff its first component lies in S and second in S₁.

Русский

Элемент пары (a,b) принадлежит prod S S₁ тогда и только тогда, когда a ∈ S и b ∈ S₁.

LaTeX

$$mem_prod : x ∈ prod S S₁ ↔ x.fst ∈ S ∧ x.snd ∈ S₁$$

Lean4

@[simp]
theorem mem_prod {S : Subalgebra R A} {S₁ : Subalgebra R B} {x : A × B} : x ∈ prod S S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁ :=
  Set.mem_prod

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