support_eq — Mathlib

English

There is a canonical CoeFun instance identifying ContDiffBump c with a real-valued function on E.

Русский

Существует каноническое соответствие ContDiffBump c с функциями над E.

LaTeX

$$$ \text{CoeFun}_{\mathbb{R}}(ContDiffBump(c), E \to \mathbb{R})$$$

Lean4

theorem support_eq : Function.support f = Metric.ball c f.rOut :=
  by
  simp only [toFun, support_comp_eq_preimage, ContDiffBumpBase.support _ _ f.one_lt_rOut_div_rIn]
  ext x
  simp only [mem_ball_iff_norm, sub_zero, norm_smul, mem_preimage, Real.norm_eq_abs, abs_inv, abs_of_pos f.rIn_pos,
    ← div_eq_inv_mul, div_lt_div_iff_of_pos_right f.rIn_pos]

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