pred_true_of_uniformOn_eq_one — Mathlib

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

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