isClosed_range_coe — Mathlib

English

The range of coefficients seen as linear maps is closed in the function space.

Русский

Область значений коэффициентов, рассмотренная как множество линейных отображений, замкнута в пространстве функций.

LaTeX

$$$\text{IsClosed}(\operatorname{range}(\text{coe} : M_1 \to M_2))$$$

Lean4

theorem isClosed_range_coe : IsClosed (Set.range ((↑) : (M₁ →ₛₗ[σ] M₂) → M₁ → M₂)) :=
  isClosed_of_closure_subset fun f hf => ⟨linearMapOfMemClosureRangeCoe f hf, rfl⟩

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