uniformOn_eq_one_of — Mathlib

English

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

Русский

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

LaTeX

$$$( \\text{uniformOn } s )(t) = 1$$$

Lean4

theorem uniformOn_eq_one_of (hs : s.Finite) (hs' : s.Nonempty) (ht : s ⊆ t) : uniformOn s t = 1 :=
  by
  haveI := uniformOn_isProbabilityMeasure hs hs'
  refine eq_of_le_of_not_lt prob_le_one ?_
  rw [not_lt, ← uniformOn_self hs hs']
  exact measure_mono ht

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