φ — Mathlib · SciLib

English

There exists a smooth bump base function u : E → ℝ with symmetric, compact support inside the unit ball and with u(−x)=u(x).

Русский

Существует гладкая функция-основание бамп‑функций u: E→ℝ с симметричной и компактной поддержкой внутри единичного шара и симметрией.

LaTeX

$$$\\exists u: E→ℝ, ContDiff ℝ ∞ u ∧ ∀ x∈ball(0,1), 0≤u(x)≤1 ∧ tsupport u = ball(0,1) ∧ u(-x)=u(x)$$$

Lean4

/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
It is the characteristic function of the closed unit ball. -/
def φ : E → ℝ :=
  (closedBall (0 : E) 1).indicator fun _ => (1 : ℝ)

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