English
If l has an antitone basis s, then for every i the family {s(j) : i ≤ j} forms 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
/-- If `f` is countably generated and `f.HasBasis p s`, then `f` admits a decreasing basis
enumerated by natural numbers such that all sets have the form `s i`. More precisely, there is a
sequence `i n` such that `p (i n)` for all `n` and `s (i n)` is a decreasing sequence of sets which
forms a basis of `f`. -/
theorem exists_antitone_subbasis {f : Filter α} [h : f.IsCountablyGenerated] {p : ι' → Prop} {s : ι' → Set α}
(hs : f.HasBasis p s) : ∃ x : ℕ → ι', (∀ i, p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i) :=
by
obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) :=
by
rcases h with ⟨s, hsc, rfl⟩
rw [generate_eq_biInf]
exact countable_biInf_principal_eq_seq_iInf hsc
have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)
let x : ℕ → { i : ι' // p i } := fun n =>
Nat.recOn n (hs.index _ <| this 0) fun n xn => hs.index _ <| inter_mem (this <| n + 1) (hs.mem_of_mem xn.2)
have x_anti : Antitone fun i => s (x i).1 :=
antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans inter_subset_right
have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
rintro (_ | i)
exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]
refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩
have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti
convert this
exact
le_antisymm (le_iInf fun i => le_principal_iff.2 <| by cases i <;> apply hs.set_index_mem)
(hx'.symm ▸ le_iInf fun i => le_principal_iff.2 <| this.1.mem_iff.2 ⟨i, trivial, x_subset i⟩)
