lift'_closure_eq_self — Mathlib

English

If l has a basis p, s and every s(i) with p i is closed, then lifting by closure yields the original filter: l.lift' closure = l.

Русский

Если у фильтра l есть базис p, s и каждый s(i) при p i замкнут, то l.lift' closure = l.

LaTeX

$$$l.HasBasis(p, s) \\\\land \\\\forall i, p i \\\\to IsClosed(s(i)) \\\\Rightarrow \\\\ l.lift' closure = l$$$

Lean4

theorem lift'_closure_eq_self {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s)
    (hc : ∀ i, p i → IsClosed (s i)) : l.lift' closure = l :=
  le_antisymm (h.ge_iff.2 fun i hi => (hc i hi).closure_eq ▸ mem_lift' (h.mem_of_mem hi)) l.le_lift'_closure

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