πJ — Mathlib

English

The map πJ is the ℤ-linear map induced by precomposition of the projection, providing a canonical linear map between LocallyConstant spaces.

Русский

Отображение πJ — это ℤ- линейное отображение, полученное пред-подстановкой проекции, обеспечивающее каноническое линейное отображение между пространствами локально константных функций.

LaTeX

$$$\\pi_J : LocallyConstant(π C (· ∈ s)) \\mathbb{Z} \\to_{\\mathbb{Z}} LocallyConstant C \\mathbb{Z}$$$

Lean4

/-- The `ℤ`-linear map induced by precomposition of the projection `C → π C (· ∈ s)`. -/
noncomputable def πJ : LocallyConstant (π C (· ∈ s)) ℤ →ₗ[ℤ] LocallyConstant C ℤ :=
  LocallyConstant.comapₗ ℤ ⟨_, (continuous_projRestrict C (· ∈ s))⟩

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