isClosed_range_coe — Mathlib

English

The range of the coe from the type of bundled multiplicative homomorphisms to plain functions is a closed subset of the function space.

Русский

Образ отображения внедрения из типа упакованных моноид-гомоморфизмов в простые функции образует.closed множество в пространстве функций.

LaTeX

$$IsClosed( Set.range (↑) )$$

Lean4

@[to_additive]
theorem isClosed_range_coe : IsClosed (Set.range ((↑) : (M₁ →ₙ* M₂) → M₁ → M₂)) :=
  isClosed_of_closure_subset fun f hf => ⟨mulHomOfMemClosureRangeCoe f hf, rfl⟩

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