Theorems · Theorem · general topology

Filter.tendsto_comp_card_atTop_iff

∀ {α : Type u_3} {β : Type u_4} [Infinite α] {f : ℕ → β} {l : Filter β},
  Filter.Tendsto (fun s => f s.card) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l

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

Defined in

Mathlib.Order.Filter.AtTopBot.Finset

Cited by

0 results in Mathlib

Foundations

Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Infinite