TendstoCofinite

📁 Source: Mathlib/Order/Filter/TendstoCofinite.lean

Statistics

Metric	Count
Definitions TendstoCofinite, mapDomain	2
Theorems comp, embedding, equiv, finite_preimage, finite_preimage_singleton, id, mapDomain_add, mapDomain_eq_zero, mapDomain_smul, tendsto_cofinite, tendstoCofinite_iff, tendstoCofinite_iff_finite_preimage_singleton, tendstoCofinite_of_finite, tendstoCofinite_of_injective, mapDomain_tendstoCofinite	15
Total	17

Filter

Definitions

Name	Category	Theorems
TendstoCofinite 📖	CompData	9 math math: Finsupp.mapDomain_tendstoCofinite, tendstoCofinite_iff_finite_preimage_singleton, TendstoCofinite.id, TendstoCofinite.embedding, TendstoCofinite.equiv, tendstoCofinite_of_finite, TendstoCofinite.comp, tendstoCofinite_iff, tendstoCofinite_of_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendstoCofinite_iff 📖	mathematical	—	TendstoCofinite Tendsto cofinite	—	—
tendstoCofinite_iff_finite_preimage_singleton 📖	mathematical	—	TendstoCofinite Set.Finite Set.preimage Set Set.instSingletonSet	—	TendstoCofinite.finite_preimage_singleton Tendsto.cofinite_of_finite_preimage_singleton
tendstoCofinite_of_finite 📖	mathematical	—	TendstoCofinite	—	tendstoCofinite_iff_finite_preimage_singleton Set.toFinite Subtype.finite
tendstoCofinite_of_injective 📖	mathematical	—	TendstoCofinite	—	Function.Injective.tendsto_cofinite

Filter.TendstoCofinite

Definitions

Name	Category	Theorems
mapDomain 📖	CompOp	3 math math: mapDomain_add, mapDomain_smul, mapDomain_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	mathematical	—	Filter.TendstoCofinite	—	Filter.tendstoCofinite_iff_finite_preimage_singleton finite_preimage
embedding 📖	mathematical	—	Filter.TendstoCofinite DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Function.Injective.tendsto_cofinite Function.Embedding.injective
equiv 📖	mathematical	—	Filter.TendstoCofinite DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	Function.Injective.tendsto_cofinite Equiv.injective
finite_preimage 📖	mathematical	—	Set.Finite Set.preimage	—	Set.compl_eq_univ_diff sdiff_sdiff_right_self inf_of_le_right tendsto_cofinite
finite_preimage_singleton 📖	mathematical	—	Set.Finite Set.preimage Set Set.instSingletonSet	—	finite_preimage
id 📖	mathematical	—	Filter.TendstoCofinite	—	—
mapDomain_add 📖	mathematical	—	mapDomain Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	finite_preimage_singleton Finset.sum_congr Finset.sum_add_distrib
mapDomain_eq_zero 📖	mathematical	Set Set.instMembership Set.range	mapDomain AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Finset.sum_congr finite_preimage_singleton Set.toFinset_congr Set.preimage_singleton_eq_empty Set.toFinset_empty
mapDomain_smul 📖	mathematical	—	mapDomain Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass	—	finite_preimage_singleton Finset.sum_congr Finset.smul_sum
tendsto_cofinite 📖	mathematical	—	Filter.Tendsto Filter.cofinite	—	—

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapDomain_tendstoCofinite 📖	mathematical	—	Filter.TendstoCofinite Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid mapDomain	—	Filter.tendstoCofinite_iff_finite_preimage_singleton Filter.TendstoCofinite.finite_preimage_singleton Set.Finite.subset Set.Finite.image finite_of_degree_le Finite.of_fintype Function.Injective.injOn Function.Embedding.injective degree_mapDomain_eq_of_subsingletonAddUnits Unique.instSubsingleton degree_comapDomain_le_of_canonicallyOrderedAdd Nat.instCanonicallyOrderedAdd embDomain_comapDomain Finset.sum_congr coe_finset_sum Finset.sum_apply single_apply Subtype.range_coe_subtype instIsConcreteLE

---

← Back to Index