generateFrom_memPartition_le — Mathlib

English

For a measurable t, generateFrom (memPartition t n) ≤ m for all n.

Русский

Для измеримого t выполняется generateFrom(memPartition t n) ≤ m для любого n.

LaTeX

$$$\forall n, generateFrom(memPartition(t,n)) \leq m$$$

Lean4

theorem generateFrom_memPartition_le [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ n, MeasurableSet (t n)) (n : ℕ) :
    generateFrom (memPartition t n) ≤ m :=
  (generateFrom_mono (subset_iUnion _ _)).trans (generateFrom_iUnion_memPartition_le ht)

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