toOuterMeasure_pure_apply — Mathlib

English

The outer measure of pure a on a set s is 1 if a ∈ s and 0 otherwise.

Русский

Общая мера чистого распределения на множество s равна 1, если a ∈ s, и 0 иначе.

LaTeX

$$$ (\mathrm{pure}\, a).\mathrm{toOuterMeasure}\, s = \begin{cases} 1, & a \in s; \\ 0, & a \notin s. \end{cases} $$$

Lean4

@[simp]
theorem toOuterMeasure_pure_apply : (pure a).toOuterMeasure s = if a ∈ s then 1 else 0 :=
  by
  refine (toOuterMeasure_apply (pure a) s).trans ?_
  split_ifs with ha
  · refine (tsum_congr fun b => ?_).trans (tsum_ite_eq a 1)
    exact ite_eq_left_iff.2 fun hb => symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)
  · refine (tsum_congr fun b => ?_).trans tsum_zero
    exact ite_eq_right_iff.2 fun hb => ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim

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