smallSets_eq_generate — Mathlib

English

The smallSets of a filter f equals the generated filter from the image of its sets under powerset: f.smallSets = generate (powerset '' f.sets).

Русский

f.smallSets равно сгенерированному фильтру от образа множества f.sets через powerset: f.smallSets = generate (powerset '' f.sets).

LaTeX

$$$f.smallSets = \mathrm{generate}(\mathrm{powerset}'' f.sets)$$$

Lean4

theorem smallSets_eq_generate {f : Filter α} : f.smallSets = generate (powerset '' f.sets) := by
  simp_rw [generate_eq_biInf, smallSets, iInf_image, Filter.lift', Filter.lift, Function.comp_apply, Filter.mem_sets]
    -- TODO: get more properties from the adjunction?
    -- TODO: is there a general way to get a lower adjoint for the lift of an upper adjoint?

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