mk_apply

Mathlib.Topology.Algebra.RestrictedProduct.Basic

URI: https://scilib.ai/kg/mathlib#RestrictedProduct.mk_apply

English

Applying mk to x with hx yields the same coordinate x_i at index i.

Русский

Применение mk к x с hx возвращает ту же координату x_i на индексе i.

LaTeX

$$$((\\mathrm{RestrictedProduct.mk}(x, hx))_i) = x_i.$$$

Lean4

@[simp]
theorem mk_apply (x : Π i, R i) (hx : ∀ᶠ i in 𝓕, x i ∈ A i) (i : ι) : (mk x hx) i = x i :=
  rfl

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

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

Разделы

Аффилиация

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