lift'_closure — Mathlib

English

If l has a basis p, s, then l.lift' closure has basis p, i ↦ closure(s(i)).

Русский

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

LaTeX

$$$\\\\text{HasBasis}(l, p, s) \\\\Rightarrow \\\\text{HasBasis}(l, p, (\\\\lambda i. \\\\overline{s(i)}))$$$

Lean4

theorem lift'_closure {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) :
    (l.lift' closure).HasBasis p fun i => closure (s i) :=
  h.lift' (monotone_closure X)

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