prod_apply

Mathlib.Topology.Algebra.Algebra

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

English

For endomorphisms f₁, f₂ and an element x ∈ A, (f₁.prod f₂)(x) = (f₁(x), f₂(x)).

Русский

Для эндоморфизмов f₁, f₂ и элемента x ∈ A выполняется (f₁.prod f₂)(x) = (f₁(x), f₂(x)).

LaTeX

$$ (f₁.prod f₂) x = (f₁ x, f₂ x) $$

Lean4

@[simp, norm_cast]
theorem prod_apply (f₁ : A →A[R] B) (f₂ : A →A[R] C) (x : A) : f₁.prod f₂ x = (f₁ x, f₂ x) :=
  rfl

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

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

Разделы

Аффилиация

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