continuous_C — Mathlib

English

The map C is continuous, i.e., the constant-coefficient embedding is continuous.

Русский

Отображение C непрерывно, то есть вложение константного коэффициента непрерывно.

LaTeX

$$Continuous (C (\sigma := σ) (R := R))$$

Lean4

@[fun_prop]
theorem continuous_C [Semiring R] : Continuous (C (σ := σ) (R := R)) := by
  classical
  simp only [continuous_iff_continuousAt]
  refine fun r ↦ (tendsto_iff_coeff_tendsto _ _ _).mpr fun d ↦ ?_
  simp only [coeff_C]
  split_ifs
  · exact tendsto_id
  · exact tendsto_const_nhds

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