map — Mathlib

English

If l has an antitone basis s, then the image filter map m l has an antitone basis given by the image of s under m.

Русский

Если у l есть антимонотонный базис s, то образующий фильтр map m l имеет антимонотонный базис, задаваемый образом m(s).

LaTeX

$$$ \text{HasAntitoneBasis}( map\ m\ l)\ (m'' s \cdot) $$$

Lean4

protected theorem map {l : Filter α} {s : ι'' → Set α} (hf : HasAntitoneBasis l s) (m : α → β) :
    HasAntitoneBasis (map m l) (m '' s ·) :=
  ⟨HasBasis.map _ hf.toHasBasis, fun _ _ h => image_mono <| hf.2 h⟩

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