coe_prod

Mathlib.Algebra.Algebra.Subalgebra.Prod

URI: https://scilib.ai/kg/mathlib#Subalgebra.coe_prod

English

The set of the product subalgebra equals the product of the sets.

Русский

Множество подалгебры произведения равно произведению множеств.

LaTeX

$$coe_prod : (prod S S₁) = (S)×(S₁)$$

Lean4

@[simp, norm_cast]
theorem coe_prod : (prod S S₁ : Set (A × B)) = (S : Set A) ×ˢ (S₁ : Set B) :=
  rfl

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

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

Разделы

Аффилиация

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