Linear_CC'₀ — Mathlib

English

The linear map Linear_CC'₀ induced by precomposition with CC'₀.

Русский

Линейное отображение Linear_CC'₀, индуцированное предсочетанием CC'₀.

LaTeX

$$Linear_CC'₀ : LocallyConstant C ℤ →ₗ[ℤ] LocallyConstant (C' C ho) ℤ$$

Lean4

/-- The `ℤ`-linear map induced by precomposing with `CC'₀` -/
noncomputable def Linear_CC'₀ : LocallyConstant C ℤ →ₗ[ℤ] LocallyConstant (C' C ho) ℤ :=
  LocallyConstant.comapₗ ℤ ⟨(CC'₀ C ho), (continuous_CC'₀ C ho)⟩

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