English
There exists a Galois insertion between the lattice of set-collections of α and the filter lattice on α, with left adjoint Generate and right adjoint Sets.
Русский
Существует Галуа-вставка между решеткой множеств над α и решеткой фильтров на α, левые и правые сопряжения заданы Generate и Sets.
LaTeX
$$$\\text{giGenerate}(\\alpha)\\ :\\ \\text{GaloisInsertion}(\\mathrm{Set}(\\mathrm{Set}(\\alpha))^{\\mathrm{op}}, \\mathrm{Filter}(\\alpha))\\text{ с левым автоадъянтом } \\operatorname{generate} \\text{ и правым } \\operatorname{sets}$$$
Lean4
/-- Galois insertion from sets of sets into filters. -/
def giGenerate (α : Type*) : @GaloisInsertion (Set (Set α)) (Filter α)ᵒᵈ _ _ Filter.generate Filter.sets
where
gc _ _ := le_generate_iff
le_l_u _ _ h := GenerateSets.basic h
choice s hs := Filter.mkOfClosure s (le_antisymm hs <| le_generate_iff.1 <| le_rfl)
choice_eq _ _ := mkOfClosure_sets
