mem_prod — Mathlib

English

An element (a,b) belongs to the product S × S1 iff a ∈ S and b ∈ S1.

Русский

Элемент (a,b) принадлежит произведению S × S1 тогда и только тогда, когда a ∈ S и b ∈ S1.

LaTeX

$$$x \\in S.prod S_1 \\iff x.first \\in S \\land x.second \\in S_1$$$

Lean4

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

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