generateFrom_le_iff — Mathlib

English

The relation generateFrom s ≤ m is equivalent to s ⊆ {t | MeasurableSet[m] t}.

Русский

Отношение generateFrom s ≤ m эквивалентно $s \subseteq \\{t \\mid MeasurableSet[m] t\\}\$.

LaTeX

$$$\\ generateFrom(s) \\le m \\iff s \\subseteq \\{t \\mid MeasurableSet[m] t\\}$$$

Lean4

theorem generateFrom_le_iff {s : Set (Set α)} (m : MeasurableSpace α) :
    generateFrom s ≤ m ↔ s ⊆ {t | MeasurableSet[m] t} :=
  Iff.intro (fun h _ hu => h _ <| measurableSet_generateFrom hu) fun h => generateFrom_le h

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