mem_prod

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalSubalgebra.mem_prod

← MathLib Explorer

English

An element (a,b) lies in S.prod S₁ iff a ∈ S and b ∈ S₁.

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru