isClosed_setOf_map_one — Mathlib

English

The set of all functions f: M1 → M2 with f(1) = 1 is a closed subset of the function space M1 → M2 (with the product topology).

Русский

множество всех функций f: M1 → M2, удовлетворяющих f(1)=1, замкнутое подмножество пространства функций M1→M2 (с произведенной топологией).

LaTeX

$$IsClosed{f : M1 → M2 | f 1 = 1}$$

Lean4

@[to_additive]
theorem isClosed_setOf_map_one [One M₁] [One M₂] : IsClosed {f : M₁ → M₂ | f 1 = 1} :=
  isClosed_eq (continuous_apply 1) continuous_const

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