comap_smallSets — Mathlib

English

Another form of smallSets for comap filters, equating to lift' with preimage and powerset.

Русский

Другая форма малого множества для фильтра-комапа, равная lift' по предобразу и мощности.

LaTeX

$$$ (\\\\mathrm{comap} f \\\\ell).smallSets = \\\\mathrm{l}.lift' (\\\\mathrm{preimage} f \\\\circ \\\\mathrm{powerset}) $$$

Lean4

theorem comap_smallSets (l : Filter β) (f : α → Set β) : comap f l.smallSets = l.lift' (preimage f ∘ powerset) :=
  comap_lift'_eq

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