Cofinite

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

Statistics

Metric	Count
Definitions cofinite	1
Theorems cofinite_of_finite_preimage_singleton, countable_compl_preimage_ker, exists_forall_ge, exists_forall_le, exists_within_forall_ge, exists_within_forall_le, atBot_le_cofinite, atTop_le_cofinite, cofinite_eq_bot, cofinite_eq_bot_iff, cofinite_inf_principal_neBot_iff, cofinite_neBot, comap_cofinite_le, coprod_cofinite, coprodᵢ_cofinite, countable_compl_ker, disjoint_cofinite_left, disjoint_cofinite_right, eventually_cofinite, eventually_cofinite_ne, frequently_cofinite_iff_infinite, frequently_cofinite_mem_iff_infinite, hasBasis_cofinite, le_cofinite_iff_compl_singleton_mem, le_cofinite_iff_eventually_ne, map_piMap_pi, map_piMap_pi_finite, mem_cofinite, univ_pi_mem_pi, eventually_cofinite_notMem, comap_cofinite_eq, nat_tendsto_atTop, tendsto_cofinite, le_map_cofinite, update_eventuallyEq, update_eventuallyEq_cofinite, cofinite_eq_atTop, eventually_pos, frequently_atTop_iff_infinite, cofinite_inf_principal_compl, cofinite_inf_principal_diff, compl_mem_cofinite, eventually_cofinite_notMem, cofinite_inf_principal_neBot, frequently_cofinite, infinite_iff_frequently_cofinite	46
Total	47

Filter

Definitions

Name	Category	Theorems
cofinite 📖	CompOp	146 math math: RestrictedProduct.single_injective, EisensteinSeries.linear_inv_isBigO_left, RestrictedProduct.mulSingle_inv, Int.cast_complex_isTheta_cast_real, IsClosed.tendsto_coe_cofinite_of_isDiscrete, mem_cofinite, frequently_cofinite_iff_infinite, Associates.finite_factors, Tendsto.cofinite_of_finite_preimage_singleton, Function.Surjective.le_map_cofinite, eventually_cofinite_ne, RestrictedProduct.mulSingle_zpow, RestrictedProduct.single_eq_zero_iff, AlgebraicGeometry.Scheme.Hom.tendsto_cofinite_cofinite, RestrictedProduct.single_mul, RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfSubgroupClassOfIsTopologicalGroupOfCompactSpaceSubtypeMem, MeasureTheory.measure_liminf_cofinite_eq_zero, comap_cofinite_le, Subgroup.tendsto_coe_cofinite_of_discrete, le_cofinite_iff_compl_singleton_mem, RestrictedProduct.isOpenEmbedding_structureMap, Function.Injective.comap_cofinite_eq, nhdsNE_le_cofinite, ModularGroup.tendsto_abs_re_smul, hasBasis_cofinite, Bornology.le_cofinite, ENNReal.tendsto_cofinite_zero_of_tsum_ne_top, cofinite.limsup_set_eq, RestrictedProduct.mul_single, RestrictedProduct.mulSingle_injective, AddSubgroup.tendsto_zmultiples_subtype_cofinite, Multipliable.tendsto_cofinite_one, RestrictedProduct.isOpen_forall_imp_mem, Set.Infinite.exists_accPt_cofinite_inf_principal, RestrictedProduct.instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem, Int.cofinite_eq, MonoidHom.tendsto_coe_cofinite_of_discrete, coLindelof_le_cofinite, CofiniteTopology.nhds_eq, RestrictedProduct.continuous_dom_prod, RestrictedProduct.isOpen_forall_mem, RestrictedProduct.mulSingle_eq_of_ne', cofinite_neBot, coprod_cofinite, le_cofinite_iff_eventually_ne, cofinite.bliminf_set_eq, eventually_cofinite, disjoint_cofinite_right, cofinite_inf_principal_neBot_iff, disjoint_cofinite_left, Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact, RestrictedProduct.coe_single_apply, MeasureTheory.measure_limsup_cofinite_eq_zero, RestrictedProduct.single_zero, RestrictedProduct.locallyCompactSpace_of_group, RestrictedProduct.comp_single, RestrictedProduct.single_add, Set.Infinite.cofinite_inf_principal_neBot, RestrictedProduct.single_sub, RestrictedProduct.mulSingle_mul, isProperMap_iff_isClosedMap_and_tendsto_cofinite, RestrictedProduct.nhds_eq_map_structureMap, Finset.eventually_cofinite_notMem, AddMonoidHom.tendsto_coe_cofinite_of_discrete, ModularGroup.tendsto_normSq_coprime_pair, Int.tendsto_zmultiplesHom_cofinite, EisensteinSeries.linear_inv_isBigO_right_add, MvPowerSeries.hasEval_def, AddSubgroup.tendsto_coe_cofinite_of_discrete, RestrictedProduct.isTopologicalRing, frequently_cofinite_mem_iff_infinite, EisensteinSeries.isBigO_linear_add_const_vec, Bornology.le_cofinite', atBot_le_cofinite, IsClosed.tendsto_coe_cofinite_of_discreteTopology, cocardinal_aleph0_eq_cofinite, Set.Finite.eventually_cofinite_notMem, tendsto_cofinite_cocompact_iff, RestrictedProduct.instContinuousMulCoeCofinite, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding', MvPowerSeries.coeff_zero_iff, Summable.tendsto_cofinite_zero, cofinite.liminf_set_eq, Asymptotics.isBigO_cofinite_iff, EisensteinSeries.linear_isTheta_left, Function.Injective.tendsto_cofinite, cofinite_eq_bot_iff, RestrictedProduct.comp_mulSingle, RestrictedProduct.coe_mulSingle_apply, RestrictedProduct.continuous_dom_pi, RestrictedProduct.single_eq_of_ne, cofinite_eq_bot, OnePoint.continuous_iff_from_discrete, Set.Finite.compl_mem_cofinite, RestrictedProduct.mulSingle_one, EisensteinSeries.linear_isTheta_right_add, ModularGroup.tendsto_lcRow0, cocompact_le_cofinite, RestrictedProduct.instLocallyCompactSpaceCoeCofiniteOfAddSubgroupClassOfIsTopologicalAddGroupOfCompactSpaceSubtypeMem, coprodᵢ_cofinite, tendsto_cofinite_cocompact_of_discrete, RestrictedProduct.single_nsmul, RestrictedProduct.continuous_dom_prod_right, Set.Infinite.frequently_cofinite, RestrictedProduct.instContinuousAddCoeCofinite, RestrictedProduct.mulSingle_pow, NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero, cofinite.blimsup_set_eq, RestrictedProduct.single_zsmul, RestrictedProduct.single_neg, RestrictedProduct.continuousSMul, RestrictedProduct.locallyCompactSpace_of_addGroup, FractionalIdeal.finite_factors', RestrictedProduct.weaklyLocallyCompactSpace_of_cofinite, EisensteinSeries.linear_isTheta_right, IsClosed.tendsto_coe_cofinite_iff, Nat.cofinite_eq_atTop, MvPowerSeries.WithPiTopology.variables_tendsto_zero, Ultrafilter.le_cofinite_or_eq_pure, cocompact_eq_cofinite, RestrictedProduct.nhds_zero_eq_map_structureMap, EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology, Int.tendsto_coe_cofinite, coclosedCompact_le_cofinite, hyperfilter_le_cofinite, FractionalIdeal.finite_factors, NonarchimedeanGroup.multipliable_iff_tendsto_cofinite_one, RestrictedProduct.continuousVAdd, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding, RestrictedProduct.isTopologicalGroup, NNReal.tendsto_cofinite_zero_of_summable, RestrictedProduct.single_eq_of_ne', EisensteinSeries.vec_add_const_isTheta, Function.update_eventuallyEq_cofinite, MvPowerSeries.HasEval.tendsto_zero, RestrictedProduct.mulSingle_div, RestrictedProduct.continuous_dom_prod_left, Set.Finite.cofinite_inf_principal_compl, RestrictedProduct.isTopologicalAddGroup, Set.infinite_iff_frequently_cofinite, RestrictedProduct.mulSingle_eq_of_ne, codiscrete_le_cofinite, Set.Finite.cofinite_inf_principal_diff, EisensteinSeries.linear_inv_isBigO_right, atTop_le_cofinite, RestrictedProduct.mulSingle_eq_one_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
atBot_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder atBot cofinite	—	le_cofinite_iff_eventually_ne eventually_ne_atBot
atTop_le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder atTop cofinite	—	le_cofinite_iff_eventually_ne eventually_ne_atTop
cofinite_eq_bot 📖	mathematical	—	cofinite Bot.bot Filter instBot	—	cofinite_eq_bot_iff
cofinite_eq_bot_iff 📖	mathematical	—	cofinite Bot.bot Filter instBot Finite	—	Set.compl_empty
cofinite_inf_principal_neBot_iff 📖	mathematical	—	NeBot Filter instInf cofinite principal Set.Infinite	—	frequently_mem_iff_neBot frequently_cofinite_mem_iff_infinite
cofinite_neBot 📖	mathematical	—	NeBot cofinite	—	HasBasis.neBot_iff hasBasis_cofinite Set.Infinite.nonempty Set.Finite.infinite_compl
comap_cofinite_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder comap cofinite	—	le_cofinite_iff_eventually_ne mem_comap Set.Finite.compl_mem_cofinite Set.finite_singleton
coprod_cofinite 📖	mathematical	—	coprod cofinite	—	coext compl_compl
coprodᵢ_cofinite 📖	mathematical	—	coprodᵢ cofinite	—	coext compl_compl
countable_compl_ker 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder cofinite	Set.Countable Compl.compl Set Set.instCompl ker	—	exists_antitone_basis HasBasis.ker HasAntitoneBasis.toHasBasis Set.iInter_true Set.compl_iInter Set.countable_iUnion instCountableNat Set.Finite.countable HasAntitoneBasis.mem
disjoint_cofinite_left 📖	mathematical	—	Disjoint Filter instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLatticeFilter cofinite Set instMembership Set.Finite	—	HasBasis.disjoint_iff_right basis_sets compl_compl
disjoint_cofinite_right 📖	mathematical	—	Disjoint Filter instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLatticeFilter cofinite Set instMembership Set.Finite	—	disjoint_comm disjoint_cofinite_left
eventually_cofinite 📖	mathematical	—	Eventually cofinite Set.Finite setOf	—	—
eventually_cofinite_ne 📖	mathematical	—	Eventually cofinite	—	Set.Finite.eventually_cofinite_notMem Set.finite_singleton
frequently_cofinite_iff_infinite 📖	mathematical	—	Frequently cofinite Set.Infinite setOf	—	—
frequently_cofinite_mem_iff_infinite 📖	mathematical	—	Frequently Set Set.instMembership cofinite Set.Infinite	—	frequently_cofinite_iff_infinite
hasBasis_cofinite 📖	mathematical	—	HasBasis Set cofinite Set.Finite Compl.compl Set.instCompl	—	Eq.subset Set.instReflSubset compl_compl Set.Finite.subset Set.compl_subset_comm
le_cofinite_iff_compl_singleton_mem 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder cofinite Set instMembership Compl.compl Set.instCompl Set.instSingletonSet	—	Set.Finite.compl_mem_cofinite Set.finite_singleton compl_compl Set.biUnion_of_singleton Set.compl_iUnion₂ biInter_mem
le_cofinite_iff_eventually_ne 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder cofinite Eventually	—	le_cofinite_iff_compl_singleton_mem
map_piMap_pi 📖	mathematical	—	map Pi.map pi	—	le_antisymm tendsto_piMap_pi tendsto_map HasBasis.ge_iff HasBasis.map hasBasis_pi basis_sets Set.univ_pi_piecewise_univ Set.piMap_image_univ_pi univ_pi_mem_pi Set.piecewise_eq_of_mem image_mem_map Set.piecewise_eq_of_notMem Set.image_univ Set.preimage_range mp_mem Set.Finite.compl_mem_cofinite univ_mem' Function.Surjective.range_eq
map_piMap_pi_finite 📖	mathematical	—	map Pi.map pi	—	map_piMap_pi cofinite_eq_bot
mem_cofinite 📖	mathematical	—	Set Filter instMembership cofinite Set.Finite Compl.compl Set.instCompl	—	—
univ_pi_mem_pi 📖	mathematical	Set Filter instMembership	pi Set.pi Set.univ	—	mp_mem pi_mem_pi univ_mem'

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofinite_of_finite_preimage_singleton 📖	mathematical	Finite Set.Elem Set.preimage Set Set.instSingletonSet	Filter.Tendsto Filter.cofinite	—	Set.Finite.preimage'
countable_compl_preimage_ker 📖	mathematical	Filter.Tendsto Filter.cofinite	Set.Countable Compl.compl Set Set.instCompl Set.preimage Filter.ker	—	Filter.ker_comap Filter.countable_compl_ker Filter.comap.isCountablyGenerated le_comap
exists_forall_ge 📖	mathematical	Filter.Tendsto Filter.cofinite Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE	—	exists_forall_le
exists_forall_le 📖	mathematical	Filter.Tendsto Filter.cofinite Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Preorder.toLE	—	exists_within_forall_le Set.univ_nonempty Set.mem_univ
exists_within_forall_ge 📖	mathematical	Set.Nonempty Filter.Tendsto Filter.cofinite Filter.atBot PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Preorder.toLE	—	exists_within_forall_le
exists_within_forall_le 📖	mathematical	Set.Nonempty Filter.Tendsto Filter.cofinite Filter.atTop PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Set Set.instMembership Preorder.toLE	—	Filter.eventually_cofinite Filter.tendsto_atTop Set.exists_min_image Set.Finite.inter_of_left lt_or_ge le_trans LT.lt.le Mathlib.Tactic.Push.not_and_eq

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_cofinite_notMem 📖	mathematical	—	Filter.Eventually Finset instMembership Filter.cofinite	—	Set.Finite.eventually_cofinite_notMem finite_toSet

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
update_eventuallyEq 📖	mathematical	—	Filter.EventuallyEq Filter.principal Compl.compl Set Set.instCompl Set.instSingletonSet update	—	Filter.mp_mem Filter.mem_principal_self Filter.univ_mem' update_of_ne
update_eventuallyEq_cofinite 📖	mathematical	—	Filter.EventuallyEq Filter.cofinite update	—	Filter.EventuallyEq.filter_mono update_eventuallyEq compl_compl

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_cofinite_eq 📖	mathematical	—	Filter.comap Filter.cofinite	—	LE.le.antisymm Filter.comap_cofinite_le Filter.Tendsto.le_comap tendsto_cofinite
nat_tendsto_atTop 📖	mathematical	—	Filter.Tendsto Filter.atTop Nat.instPreorder	—	tendsto_cofinite Nat.cofinite_eq_atTop
tendsto_cofinite 📖	mathematical	—	Filter.Tendsto Filter.cofinite	—	Set.Finite.preimage injOn

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_map_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.cofinite Filter.map	—	Set.Finite.of_preimage

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofinite_eq_atTop 📖	mathematical	—	Filter.cofinite Filter.atTop instPreorder	—	le_antisymm Filter.HasBasis.ge_iff Filter.atTop_basis SemilatticeSup.instIsDirectedOrder Set.compl_Ici Set.finite_lt_nat Filter.atTop_le_cofinite instNoTopOrderOfNoMaxOrder instNoMaxOrder
eventually_pos 📖	mathematical	—	Filter.Eventually Filter.atTop instPreorder	—	Filter.eventually_of_mem Filter.mem_atTop_sets SemilatticeSup.instIsDirectedOrder
frequently_atTop_iff_infinite 📖	mathematical	—	Filter.Frequently Filter.atTop instPreorder Set.Infinite setOf	—	cofinite_eq_atTop Filter.frequently_cofinite_iff_infinite

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite_iff_frequently_cofinite 📖	mathematical	—	Infinite Filter.Frequently Set instMembership Filter.cofinite	—	Filter.frequently_cofinite_iff_infinite

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofinite_inf_principal_compl 📖	mathematical	—	Filter Filter.instInf Filter.cofinite Filter.principal Compl.compl Set Set.instCompl	—	compl_compl compl_mem_cofinite
cofinite_inf_principal_diff 📖	mathematical	—	Filter Filter.instInf Filter.cofinite Filter.principal Set Set.instSDiff	—	Set.diff_eq Filter.inf_principal inf_assoc inf_right_comm cofinite_inf_principal_compl
compl_mem_cofinite 📖	mathematical	—	Set Filter Filter.instMembership Filter.cofinite Compl.compl Set.instCompl	—	Filter.mem_cofinite compl_compl
eventually_cofinite_notMem 📖	mathematical	—	Filter.Eventually Set Set.instMembership Filter.cofinite	—	compl_mem_cofinite

Set.Infinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cofinite_inf_principal_neBot 📖	mathematical	Set.Infinite	Filter.NeBot Filter Filter.instInf Filter.cofinite Filter.principal	—	Filter.cofinite_inf_principal_neBot_iff
frequently_cofinite 📖	mathematical	Set.Infinite	Filter.Frequently Set Set.instMembership Filter.cofinite	—	Filter.frequently_cofinite_mem_iff_infinite

---

← Back to Index