generateFrom_generatePiSystem_eq — Mathlib

English

The generated-from relation commutes with generatePiSystem: generateFrom (generatePiSystem g) = generateFrom g.

Русский

Операция generateFrom и generatePiSystem взаимно согласованы: generateFrom (generatePiSystem g) = generateFrom g.

LaTeX

$$$$ \mathrm{generateFrom}\left(\mathrm{generatePiSystem}(g)\right) = \mathrm{generateFrom}(g) $$$$

Lean4

theorem generateFrom_generatePiSystem_eq {g : Set (Set α)} : generateFrom (generatePiSystem g) = generateFrom g :=
  by
  apply le_antisymm <;> apply generateFrom_le
  · exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t
  · exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)

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