English
If l has an antitone basis s, φ is a monotone map with Tendsto φ atTop, then the composition s ∘ φ is again an antitone basis for l.
Русский
Если у l есть антитональная база s, отображение φ монотонно и Tendsto φ к atTop, тогда композиция s ∘ φ тоже антитональная база для l.
LaTeX
$$$$l.HasAntitoneBasis s \Rightarrow (Monotone\, φ) \Rightarrow (Tendsto\, φ\ atTop\ atTop) \Rightarrow l.HasAntitoneBasis (s \circ φ)$$$$
Lean4
theorem comp_mono [Nonempty ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Preorder ι'] {l : Filter α} {s : ι' → Set α}
(hs : l.HasAntitoneBasis s) {φ : ι → ι'} (φ_mono : Monotone φ) (hφ : Tendsto φ atTop atTop) :
l.HasAntitoneBasis (s ∘ φ) :=
⟨hs.1.to_hasBasis (fun n _ => (hφ.eventually_ge_atTop n).exists.imp fun _m hm => ⟨trivial, hs.antitone hm⟩) fun n _ =>
⟨φ n, trivial, Subset.rfl⟩,
hs.antitone.comp_monotone φ_mono⟩
