instStar — Mathlib

English

For any compactly supported continuous map f: α → β, the star operation commutes with the evaluation, i.e., (star f)(x) = star(f(x)) for all x ∈ α.

Русский

Для любого компактно поддерживаемого непрерывного отображения f: α → β звёздочка применяется по точке: (star f)(x) = star(f(x)) для всех x ∈ α.

LaTeX

$$$ (\mathrm{star} f)(x) = \mathrm{star}(f(x)) $ for all x$$

Lean4

instance : Star C_c(α, β) where
  star
    f :=
    { toFun := fun x => star (f x)
      continuous_toFun := (map_continuous f).star
      hasCompactSupport' := by
        rw [HasCompactSupport, tsupport]
        have support_star : (Function.support fun (x : α) => star (f x)) = Function.support f :=
          by
          ext x
          simp only [Function.mem_support, ne_eq, star_eq_zero]
        rw [support_star]
        exact f.2 }

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