Theorems · Inductive type · general topology
Filter.TendstoCofinite
{α : Type u_1} → {β : Type u_2} → (α → β) → PropThe class of functions f such that Tendsto f cofinite cofinite, it is equivalent to
f having finite fibers, see Filter.tendstoCofinite_iff_finite_preimage_singleton.
- Defined in
- Mathlib.Order.Filter.TendstoCofinite
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by33
Results whose statement or proof uses this declaration.
- MvPowerSeries.renamestatement and proof · cited by 26
- Filter.TendstoCofinite.finite_preimage_singletonstatement and proof · cited by 12
- MvPowerSeries.coeff_renamestatement and proof · cited by 7
- Filter.TendstoCofinite.mapDomainstatement and proof · cited by 4
- MvPowerSeries.rename_renamestatement and proof · cited by 3
- MvPowerSeries.rename_Cstatement and proof · cited by 2
- MvPowerSeries.rename_Xstatement and proof · cited by 2
- MvPowerSeries.rename_eq_subststatement and proof · cited by 2
- MvPowerSeries.rename_monomialstatement and proof · cited by 2
- MvPowerSeries.HasSubst.X_compstatement and proof · cited by 1
- Filter.tendstoCofinite_iff_finite_preimage_singletonstatement and proof · cited by 1
- Filter.TendstoCofinite.casesOnstatement and proof · cited by 1