fst_prod_snd

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#ContinuousAlgHom.fst_prod_snd

English

The composition of fst with the product of f and g equals the identity on A×B.

Русский

Сочетание fst с произведением f и g равно тождественному отображению на A×B.

LaTeX

$$$(fst R A B).prod (snd R A B) = id R (A × B)$$$

Lean4

@[simp]
theorem fst_prod_snd : (fst R A B).prod (snd R A B) = ContinuousAlgHom.id R (A × B) :=
  ext fun ⟨_x, _y⟩ => rfl

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

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

Разделы

Аффилиация

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