lift'_interior — Mathlib

English

If l has a basis p and s, then the lifted filter (l.lift' interior) has basis p with interiors of s(i).

Русский

Если у фильтра l есть базис p и s, то подъем l.lift' interior имеет базис p с interior(s(i)).

LaTeX

$$$ h:\, l.HasBasis\ p\ s\Rightarrow (l.lift' \operatorname{int}).HasBasis p \ (\lambda i. \operatorname{int}(s(i)))$$$

Lean4

theorem lift'_interior {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) :
    (l.lift' interior).HasBasis p fun i => interior (s i) :=
  h.lift' fun _ _ ↦ interior_mono

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