English
There is a Galois insertion between σ-algebras on α and Set(Set α) using generateFrom and the set of measurable sets.
Русский
Существует галуа-инсерция между сигма-алгебрами на α и множеством подмножеств ее надмножеств, используя generateFrom и множества измеримых.
LaTeX
$$$\\text{giGenerateFrom} : GaloisInsertion(\\text{generateFrom},\\lambda m.\\{t\\mid MeasurableSet[m] t\\})$$$
Lean4
/-- We get a Galois insertion between `σ`-algebras on `α` and `Set (Set α)` by using `generate_from`
on one side and the collection of measurable sets on the other side. -/
def giGenerateFrom : GaloisInsertion (@generateFrom α) fun m => {t | MeasurableSet[m] t}
where
gc _ := generateFrom_le_iff
le_l_u _ _ := measurableSet_generateFrom
choice g hg := MeasurableSpace.mkOfClosure g <| le_antisymm hg <| (generateFrom_le_iff _).1 le_rfl
choice_eq _ _ := mkOfClosure_sets
