generateFrom_countablePartition_le_succ

English

For α with a countably generated measurable space, the sigma-algebra generated by the n-th partition is contained in the sigma-algebra generated by the (n+1)-st partition: generateFrom (countablePartition α n) ≤ generateFrom (countablePartition α (n+1)).

Русский

Пусть α имеет счетно генерируемое измеримое пространство. Тогда сигма-алгебра, порождаемая n-й частью разбиения, содержится в сигма-алгебре, порождаемой (n+1)-й частью: generateFrom(countablePartition α n) ≤ generateFrom(countablePartition α (n+1)).

LaTeX

$$$$ \\operatorname{generateFrom}(\\operatorname{countablePartition}(\\alpha,n)) \\le \\operatorname{generateFrom}(\\operatorname{countablePartition}(\\alpha,(n+1))). $$$$

Lean4

theorem generateFrom_countablePartition_le_succ (α : Type*) [MeasurableSpace α] [CountablyGenerated α] (n : ℕ) :
    generateFrom (countablePartition α n) ≤ generateFrom (countablePartition α (n + 1)) :=
  generateFrom_memPartition_le_succ _ _

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