English
If a monotone function from a preorder to Finset α covers all elements eventually, then it tends to atTop as well.
Русский
Если функция монотонна и охватывает все элементы в пределе, она стремится к atTop.
LaTeX
$$$[\text{Preorder } β] \; f: β \to \text{Finset } α, \; h: \text{Monotone } f, \; (\forall x:α, \exists n, x \in f(n)) \\Rightarrow \operatorname{Tendsto} f \operatorname{atTop} \operatorname{atTop}$$$
Lean4
/-- Given an antitone basis `s : ℕ → Set α` of a filter, extract an antitone subbasis `s ∘ φ`,
`φ : ℕ → ℕ`, such that `m < n` implies `r (φ m) (φ n)`. This lemma can be used to extract an
antitone basis with basis sets decreasing "sufficiently fast". -/
theorem subbasis_with_rel {f : Filter α} {s : ℕ → Set α} (hs : f.HasAntitoneBasis s) {r : ℕ → ℕ → Prop}
(hr : ∀ m, ∀ᶠ n in atTop, r m n) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ (∀ ⦃m n⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ) :=
by
rsuffices ⟨φ, hφ, hrφ⟩ : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ m n, m < n → r (φ m) (φ n)
· exact ⟨φ, hφ, hrφ, hs.comp_strictMono hφ⟩
have : ∀ t : Set ℕ, t.Finite → ∀ᶠ n in atTop, ∀ m ∈ t, m < n ∧ r m n := fun t ht =>
(eventually_all_finite ht).2 fun m _ => (eventually_gt_atTop m).and (hr _)
rcases seq_of_forall_finite_exists fun t ht => (this t ht).exists with ⟨φ, hφ⟩
simp only [forall_mem_image, forall_and, mem_Iio] at hφ
exact ⟨φ, forall_swap.2 hφ.1, forall_swap.2 hφ.2⟩
