coeFn_eq_comp — Mathlib

English

The function thickenedIndicator δ_pos E is equal to ENNReal.toNNReal composed with thickenedIndicatorAux δ E.

Русский

Функция thickenedIndicator δ_pos E равна ENNReal.toNNReal ∘ thickenedIndicatorAux δ E.

LaTeX

$$$\forall δ\in \mathbb{R},\; δ_{pos}>0:\; \text{coe}(thickenedIndicator(δ,E)) = (\operatorname{ENNReal.toNNReal}) \circ \operatorname{thickenedIndicatorAux}(δ,E)$$$

Lean4

theorem coeFn_eq_comp {δ : ℝ} (δ_pos : 0 < δ) (E : Set α) :
    ⇑(thickenedIndicator δ_pos E) = ENNReal.toNNReal ∘ thickenedIndicatorAux δ E :=
  rfl

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