Filter.atTop and Filter.atBot filters and finite sets.

theorem Filter.tendsto_finset_range : Tendsto Finset.range atTop atTop

theorem Filter.atTop_finset_eq_iInf {α : Type u_3} : atTop = ⨅ (x : α), principal (Set.Ici {x})

theorem Filter.tendsto_atTop_finset_of_monotone {α : Type u_3} {β : Type u_4} [Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ (x : α), ∃ (n : β), x ∈ f n) : Tendsto f atTop atTop

If f is a monotone sequence of Finsets and each x belongs to one of f n, then Tendsto f atTop atTop.

theorem Monotone.tendsto_atTop_finset {α : Type u_3} {β : Type u_4} [Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ (x : α), ∃ (n : β), x ∈ f n) : Filter.Tendsto f Filter.atTop Filter.atTop

Alias of Filter.tendsto_atTop_finset_of_monotone.

---

If f is a monotone sequence of Finsets and each x belongs to one of f n, then Tendsto f atTop atTop.

theorem Filter.tendsto_finset_image_atTop_atTop {β : Type u_4} {γ : Type u_5} [DecidableEq β] {i : β → γ} {j : γ → β} (h : Function.LeftInverse j i) : Tendsto (Finset.image j) atTop atTop

theorem Filter.tendsto_finset_preimage_atTop_atTop {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) : Tendsto (fun (s : Finset β) => s.preimage f ⋯) atTop atTop

theorem Filter.tendsto_toLeft_atTop {α : Type u_3} {β : Type u_4} : Tendsto Finset.toLeft atTop atTop

theorem Filter.tendsto_toRight_atTop {α : Type u_3} {β : Type u_4} : Tendsto Finset.toRight atTop atTop