uniformOn_singleton — Mathlib

English

For a singleton ω, uniformOn {ω} t equals 1 if ω ∈ t, and 0 otherwise.

Русский

Для множества-единства {ω} мера равномерна на t так, что значение равно 1 если ω ∈ t и 0 иначе.

LaTeX

$$$uniformOn\{\omega\}(t) = \begin{cases}1, & \omega \in t \\ 0, & \omega \notin t\end{cases}$$$

Lean4

theorem uniformOn_singleton (ω : Ω) (t : Set Ω) [Decidable (ω ∈ t)] : uniformOn { ω } t = if ω ∈ t then 1 else 0 :=
  by
  rw [uniformOn, cond_apply (measurableSet_singleton ω), Measure.count_singleton, inv_one, one_mul]
  split_ifs
  · rw [(by simpa : ({ ω } : Set Ω) ∩ t = { ω }), Measure.count_singleton]
  · simpa

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