uniformOn_self — Mathlib

English

If s is finite, nonempty and s ⊆ t, then uniformOn s t = 1.

Русский

Если s конечна и непуста и s ⊆ t, то uniformOn s t = 1.

LaTeX

$$$uniformOn s t = 1$ under $s\subseteq t$ with $s$ finite and nonempty.$$

Lean4

theorem uniformOn_self (hs : s.Finite) (hs' : s.Nonempty) : uniformOn s s = 1 :=
  by
  rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
  · rwa [Measure.count_ne_zero_iff]
  · exact (Measure.count_apply_lt_top.2 hs).ne

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