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_2} : atTop = ⨅ (x : α), principal (Set.Ici {x})

theorem Filter.tendsto_atTop_finset_of_monotone {α : Type u_2} {β : Type u_3} [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_2} {β : Type u_3} [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_3} {γ : Type u_4} [DecidableEq β] {i : β → γ} {j : γ → β} (h : Function.LeftInverse j i) : Tendsto (Finset.image j) atTop atTop

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

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

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

theorem Filter.tendsto_finset_powerset_atTop_atTop {α : Type u_2} : Tendsto Finset.powerset atTop atTop

theorem Filter.tendsto_finset_Iic_atTop_atTop {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] : Tendsto Finset.Iic atTop atTop

theorem Filter.tendsto_finset_Ici_atBot_atTop {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] : Tendsto Finset.Ici atBot atTop

theorem Filter.eventually_finset_atTop_subset {α : Type u_2} (i : Finset α) : ∀ᶠ (s : Finset α) in atTop, i ⊆ s

Every finset is eventually a subset of s along atTop.

theorem Filter.eventually_finset_mem_atTop {α : Type u_2} (i : α) : ∀ᶠ (s : Finset α) in atTop, i ∈ s

Every element of α is eventually a member of s along atTop on Finset α.

theorem Filter.map_card_atTop {α : Type u_2} [Infinite α] : map Finset.card atTop = atTop

The pushforward of atTop on Finset α along Finset.card is atTop on ℕ, when α is infinite.

theorem Filter.map_card_atTop_of_fintype {α : Type u_2} [Fintype α] : map Finset.card atTop = pure (Fintype.card α)

The pushforward of atTop on Finset α along Finset.card is pure (Fintype.card α), when α is finite.

theorem Filter.tendsto_card_atTop_atTop {α : Type u_2} [Infinite α] : Tendsto Finset.card atTop atTop

Finset.card tends to atTop along atTop on Finset α, when α is infinite.

theorem Filter.tendsto_card_atTop_pure_of_fintype {α : Type u_2} [Fintype α] : Tendsto Finset.card atTop (pure (Fintype.card α))

Finset.card tends to pure (Fintype.card α), when α is finite.

theorem Filter.tendsto_comp_card_atTop_iff {α : Type u_2} {β : Type u_3} [Infinite α] {f : ℕ → β} {l : Filter β} : Tendsto (fun (s : Finset α) => f s.card) atTop l ↔ Tendsto f atTop l

Tendsto along atTop for a function precomposed with Finset.card reduces to Tendsto along atTop on ℕ, when α is infinite.

theorem Filter.tendsto_comp_card_atTop_iff_of_fintype {α : Type u_2} {β : Type u_3} [Fintype α] {f : ℕ → β} {l : Filter β} : Tendsto (fun (s : Finset α) => f s.card) atTop l ↔ Tendsto f (pure (Fintype.card α)) l

Tendsto along atTop for a function precomposed with Finset.card reduces to Tendsto along pure (Fintype.card α), when α is finite.