English
If f is monotone and each element belongs to some f(n), then f tends to atTop.
Русский
Если f монотонна и каждый элемент принадлежит некоторому f(n), тогда f стремится к 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
/-- If `f` is a monotone sequence of `Finset`s and each `x` belongs to one of `f n`, then
`Tendsto f atTop atTop`. -/
theorem tendsto_atTop_finset_of_monotone [Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ x : α, ∃ n, x ∈ f n) :
Tendsto f atTop atTop :=
by
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
intro a
rcases h' a with ⟨b, hb⟩
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')
