isClosed_range_coe — Mathlib

English

The range of the coercion from M₁ →* M₂ to M₁ → M₂ is closed in the function space.

Русский

Образ внедрения MonoidHom M₁ →* M₂ в M₁ → M₂ замкнут в пространстве функций.

LaTeX

$$IsClosed (Set.range MonoidHom.instFunLike.coe)$$

Lean4

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

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