w_support — Mathlib

English

If D>0, then w(D) has compact support.

Русский

Если D>0, то у функции w есть компактная опора.

LaTeX

$$HasCompactSupport (w(D))$$

Lean4

theorem w_support {D : ℝ} (Dpos : 0 < D) : support (w D : E → ℝ) = ball 0 D :=
  by
  have B : D • ball (0 : E) 1 = ball 0 D := by rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
  have C : D ^ finrank ℝ E ≠ 0 := by
    norm_cast
    exact pow_ne_zero _ Dpos.ne'
  simp only [w_def, Algebra.id.smul_eq_mul, support_mul, support_inv, univ_inter, support_comp_inv_smul₀ Dpos.ne',
    u_support, B, support_const (u_int_pos E).ne', support_const C, abs_of_nonneg Dpos.le]

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