isClosed_setOf_map_mul — Mathlib

English

The set of all functions f: M1 → M2 that preserve multiplication, i.e., f(xy) = f(x) f(y) for all x,y, is closed in the function space M1 → M2.

Русский

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

LaTeX

$$IsClosed{f : M1 → M2 | ∀ x y, f(x y) = f(x) f(y)}$$

Lean4

@[to_additive]
theorem isClosed_setOf_map_mul [Mul M₁] [Mul M₂] [ContinuousMul M₂] :
    IsClosed {f : M₁ → M₂ | ∀ x y, f (x * y) = f x * f y} :=
  by
  simp only [setOf_forall]
  exact isClosed_iInter fun x ↦ isClosed_iInter fun y ↦ isClosed_eq (continuous_apply _) (by fun_prop)

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