uniformOn_eq_zero_iff — Mathlib

English

For finite s, uniformOn s t = 0 if and only if s ∩ t = ∅.

Русский

Для конечного s верно: uniformOn s t = 0 тогда и только тогда, когда s ∩ t = ∅.

LaTeX

$$$uniformOn\\; s\\; t = 0 \\iff s \\cap t = \\varnothing$$$

Lean4

theorem uniformOn_eq_zero_iff (hs : s.Finite) : uniformOn s t = 0 ↔ s ∩ t = ∅ := by
  simp [uniformOn, cond_apply hs.measurableSet, Measure.count_apply_eq_top, Set.not_infinite.2 hs,
    Measure.count_apply_finite _ (hs.inter_of_left _)]

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