English
If s is finite nonempty then uniformOn s Set.univ = 1.
Русский
Если s конечна и непустa, то uniformOn s Set.univ = 1.
LaTeX
$$$uniformOn\\; s\\; Set.univ = 1$$$
Lean4
theorem pred_true_of_uniformOn_eq_one (h : uniformOn s t = 1) : s ⊆ t :=
by
have hsf := finite_of_uniformOn_ne_zero (by rw [h]; exact one_ne_zero)
rw [uniformOn, cond_apply hsf.measurableSet, mul_comm] at h
replace h := ENNReal.eq_inv_of_mul_eq_one_left h
rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _), Nat.cast_inj] at h
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge