prod_eval

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.prod_eval

English

Let f: α → β1 and g: α → β2 be continuous, and a ∈ α. Then (prodMk f g) a = (f a, g a).

Русский

Пусть f: α → β1 и g: α → β2 непрерывны, и a ∈ α. Тогда (prodMk f g) a = (f(a), g(a)).

LaTeX

$$$(\mathrm{prodMk}(f,g))(a)=(f(a),g(a))$$$

Lean4

@[simp]
theorem prod_eval (f : C(α, β₁)) (g : C(α, β₂)) (a : α) : (prodMk f g) a = (f a, g a) :=
  rfl

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

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

Разделы

Аффилиация

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