Structures · Order
Filter.TendstoCofinite
The 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
- Shape
- One type argument · adds tendsto_cofinite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- Finsupp
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- MvPowerSeries.rename
- Filter.TendstoCofinite.finite_preimage_singleton
- MvPowerSeries.coeff_rename
- Filter.TendstoCofinite.mapDomain
- MvPowerSeries.rename_rename
- MvPowerSeries.rename_X
- MvPowerSeries.rename_C
- MvPowerSeries.rename_eq_subst
- MvPowerSeries.rename_monomial
- Filter.TendstoCofinite.tendsto_cofinite
- MvPowerSeries.rename_comp_toMvPowerSeries
- Filter.TendstoCofinite.finite_preimage
- MvPowerSeries.HasSubst.X_comp
- MvPowerSeries.renameFun
- MvPowerSeries.constantCoeff_rename
- Filter.TendstoCofinite.mapDomain_smul
- Filter.TendstoCofinite.mapDomain.congr_simp
- MvPowerSeries.coeff_rename_eq_zero
- Northcott.comp_of_finite_fibers
- Finsupp.mapDomain_tendstoCofinite
- MvPowerSeries.rename_map
- Filter.TendstoCofinite.mapDomain_add
- MvPowerSeries.renameFun.congr_simp
- Filter.TendstoCofinite.comp
- MvPowerSeries.rename_toMvPowerSeries
- MvPowerSeries.rename_comp_rename
- Filter.TendstoCofinite.mapDomain_eq_zero
- MvPowerSeries.rename.congr_simp
- MvPowerSeries.rename_coe
Ancestors0
No ancestors.