hasBasis_ge — Mathlib

English

Assume l has an antitone basis s; for every i, the tail form {s(j) : i ≤ j} is a basis for l.

Русский

Пусть l имеет антитонное основание s; для каждого i множество {s(j) : i ≤ j} образует базис l.

LaTeX

$$$\\mathrm{HasAntitoneBasis}(l,s)\\rightarrow \\forall i\\, l.HasBasis(\\lambda j. i\\le j)\\ s$$$

Lean4

theorem hasBasis_ge [Preorder ι] [IsDirected ι (· ≤ ·)] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s)
    (i : ι) : l.HasBasis (fun j => i ≤ j) s :=
  hs.1.to_hasBasis (fun j _ => (exists_ge_ge i j).imp fun _k hk => ⟨hk.1, hs.2 hk.2⟩) fun j _ =>
    ⟨j, trivial, Subset.rfl⟩

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