bind_smallSets_gc — Mathlib

English

There is a Galois connection between the operation L ↦ L.bind principal on Filter (Set α) and the smallSets operator on Filter α.

Русский

Существует связь Галуа между операцией L ↦ L.bind principal на Filter(Set α) и оператором smallSets на Filter α.

LaTeX

$$GaloisConnection (fun L : Filter (Set α) => L.bind principal) smallSets$$

Lean4

theorem bind_smallSets_gc : GaloisConnection (fun L : Filter (Set α) ↦ L.bind principal) smallSets :=
  by
  intro L l
  simp_rw [smallSets_eq_generate, le_generate_iff, image_subset_iff]
  rfl

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