indicatorConstLp_empty — Mathlib

English

If s is empty, indicatorConstLp(p, s, hμs, c) is identically zero for all p and μ with μ∅ finite.

Русский

Если s пусто, indicatorConstLp(p, s, hμs, c) тождественно равно нулю.

LaTeX

$$$indicatorConstLp(p, \varnothing, hμs, c) = 0$.$$

Lean4

@[simp]
theorem indicatorConstLp_empty : indicatorConstLp p MeasurableSet.empty (by simp : μ ∅ ≠ ∞) c = 0 := by
  simp only [indicatorConstLp, Set.indicator_empty', MemLp.toLp_zero]

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