measure_biUnion_finset_le — Mathlib

English

For a Finset I and s : I → Set α, μ(⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ(s i).

Русский

Для конечного множества I и функций s: I → Set α, μ(⋃ i ∈ I, s i) ≤ ∑ i ∈ I μ(s i).

LaTeX

$$$\forall I : Finset\ ι,\; μ(\bigcup_{i \in I} s i) \le \sum_{i \in I} μ(s i)$$$

Lean4

theorem measure_biUnion_finset_le (I : Finset ι) (s : ι → Set α) : μ (⋃ i ∈ I, s i) ≤ ∑ i ∈ I, μ (s i) :=
  (measure_biUnion_le μ I.countable_toSet s).trans_eq <| I.tsum_subtype (μ <| s ·)

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