Linear_CC'₁ — Mathlib

English

The linear map Linear_CC' is the difference between Linear_CC'₁ and Linear_CC'₀.

Русский

Линейное отображение Linear_CC' есть разность Linear_CC'₁ и Linear_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 hsC ho), (continuous_CC'₁ C hsC ho)⟩

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