dirac_apply_of_mem — Mathlib

English

Let a be a point in a measurable space. The Dirac measure δ_a assigns unit mass to any measurable set that contains a; equivalently δ_a(s) = 1 if a ∈ s, and 0 otherwise.

Русский

Пусть a — точка пространства с мерой. Мера Дирака δ_a присваивает единичную массу любому измеримому множеству, которое содержит a; эквивалентно δ_a(s) = 1 если a ∈ s и 0 иначе.

LaTeX

$$$ a \\in s \\Rightarrow dirac a s = 1 $$$

Lean4

@[simp]
theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1 :=
  by
  have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
  refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)
  rw [← dirac_apply' a MeasurableSet.univ]
  exact measure_mono (subset_univ s)

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