SmallSets

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

Statistics

Metric	Count
Definitions smallSets	1
Theorems exists_mem_basis_of_smallSets, exists_mem_of_smallSets, of_smallSets, smallSets, smallSets_of_forall_mem_basis, tendsto_smallSets, eventually_smallSets, frequently_smallSets, smallSets, image_smallSets, of_smallSets, smallSets_mono, bind_smallSets_gc, comap_smallSets, eventually_smallSets, eventually_smallSets', eventually_smallSets_eventually, eventually_smallSets_forall, eventually_smallSets_subset, frequently_smallSets, frequently_smallSets', frequently_smallSets_mem, hasBasis_smallSets, monotone_smallSets, smallSets_bot, smallSets_comap, smallSets_comap_eq_comap_image, smallSets_eq_generate, smallSets_iInf, smallSets_inf, smallSets_neBot, smallSets_principal, smallSets_top, tendsto_image_smallSets, tendsto_smallSets_iff	35
Total	36

Filter

Definitions

Name	Category	Theorems
smallSets 📖	CompOp	58 math math: smallSets_eq_generate, Bornology.isVonNBounded_iff_tendsto_smallSets_nhds, locallyFinite_iff_smallSets, Tendsto.uIcc, Asymptotics.IsLittleOTVS.eventually_smallSets, bind_smallSets_gc, Tendsto.Icc, Tendsto.image_smallSets, smallSets_comap_eq_comap_image, frequently_smallSets_mem, TendstoIxxClass.tendsto_Ixx, HasBasis.frequently_smallSets, smallSets_neBot, Asymptotics.isBigOTVS_iff_smallSets, comap_smallSets, MeasureTheory.Measure.mem_support_iff, Tendsto.Ioc, eventually_smallSets, MeasureTheory.Measure.notMem_support_iff, eventually_smallSets_forall, Bornology.IsVonNBounded.tendsto_smallSets_nhds, tendsto_smallSets_iff, MeasureTheory.UnifTight.eventually_cofinite_indicator, Asymptotics.isLittleOTVS_iff_smallSets, ContDiffWithinAt.eventually_hasFTaylorSeriesUpToOn, StronglyMeasurableAtFilter.eventually, smallSets_bot, smallSets_top, Eventually.smallSets, smallSets_comap, Asymptotics.IsBigOTVS.eventually_smallSets, Frequently.smallSets_of_forall_mem_basis, eventually_uniformity_iterate_comp_subset, MeasureTheory.Measure.mem_support_restrict, tendsto_closedBall_smallSets, frequently_smallSets', HasBasis.smallSets, eventually_smallSets_eventually, monotone_smallSets, MeasureTheory.Measure.FiniteAtFilter.eventually, frequently_smallSets, Tendsto.Ioo, tendsto_image_smallSets, smallSets_iInf, smallSets_inf, ContDiffBump.tendsto_support_normed_smallSets, bsupr_limsup_dimH, eventually_smallSets_subset, smallSets_principal, HasBasis.eventually_smallSets, HasAntitoneBasis.tendsto_smallSets, MeasureTheory.IntegrableAtFilter.eventually, eventually_smallSets', LocallyFinite.eventually_smallSets, hasBasis_smallSets, iSup_limsup_dimH, Tendsto.Ico, eventually_uniformity_comp_subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bind_smallSets_gc 📖	mathematical	—	GaloisConnection Filter Set PartialOrder.toPreorder instPartialOrder bind principal smallSets	—	smallSets_eq_generate
comap_smallSets 📖	mathematical	—	comap Set smallSets lift' Set.preimage Set.powerset	—	comap_lift'_eq
eventually_smallSets 📖	mathematical	—	Eventually Set smallSets Filter instMembership	—	eventually_lift'_iff Set.monotone_powerset
eventually_smallSets' 📖	mathematical	—	Eventually Set smallSets Filter instMembership	—	eventually_smallSets Iff.and Set.Subset.rfl
eventually_smallSets_eventually 📖	mathematical	—	Eventually Set smallSets Filter instInf	—	eventually_smallSets' Eventually.mono
eventually_smallSets_forall 📖	mathematical	—	Eventually Set smallSets	—	inf_top_eq eventually_smallSets_eventually
eventually_smallSets_subset 📖	mathematical	—	Eventually Set Set.instHasSubset smallSets Filter instMembership	—	eventually_smallSets_forall
frequently_smallSets 📖	mathematical	—	Frequently Set smallSets Set.instHasSubset	—	HasBasis.frequently_iff hasBasis_smallSets
frequently_smallSets' 📖	mathematical	—	Frequently Set smallSets	—	not_iff_not eventually_smallSets'
frequently_smallSets_mem 📖	mathematical	—	Frequently Set Filter instMembership smallSets	—	frequently_smallSets Set.Subset.rfl
hasBasis_smallSets 📖	mathematical	—	HasBasis Set smallSets Filter instMembership Set.powerset	—	HasBasis.smallSets basis_sets
monotone_smallSets 📖	mathematical	—	Monotone Filter Set PartialOrder.toPreorder instPartialOrder smallSets	—	monotone_lift' monotone_id monotone_const
smallSets_bot 📖	mathematical	—	smallSets Bot.bot Filter instBot instPure Set Set.instEmptyCollection	—	smallSets.eq_1 lift'_bot Set.monotone_powerset Set.powerset_empty principal_singleton
smallSets_comap 📖	mathematical	—	smallSets comap lift' Set Set.powerset Set.preimage	—	comap_lift'_eq2 Set.monotone_powerset
smallSets_comap_eq_comap_image 📖	mathematical	—	smallSets comap Set Set.image	—	GaloisConnection.u_comm_of_l_comm gc_map_comap bind_smallSets_gc map_principal
smallSets_eq_generate 📖	mathematical	—	smallSets generate Set Set.image Set.powerset sets	—	generate_eq_biInf iInf_image iInf_congr_Prop
smallSets_iInf 📖	mathematical	—	smallSets iInf Filter instInfSet Set	—	lift'_iInf_of_map_univ Set.powerset_inter Set.powerset_univ
smallSets_inf 📖	mathematical	—	smallSets Filter instInf Set	—	lift'_inf Set.powerset_inter
smallSets_neBot 📖	mathematical	—	NeBot Set smallSets	—	lift'_neBot_iff Set.monotone_powerset Set.powerset_nonempty
smallSets_principal 📖	mathematical	—	smallSets principal Set Set.powerset	—	lift'_principal Set.monotone_powerset
smallSets_top 📖	mathematical	—	smallSets Top.top Filter instTop Set	—	smallSets.eq_1 lift'_top Set.powerset_univ principal_univ
tendsto_image_smallSets 📖	mathematical	—	Tendsto Set Set.image smallSets	—	tendsto_smallSets_iff eventually_smallSets' HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono
tendsto_smallSets_iff 📖	mathematical	—	Tendsto Set smallSets Eventually Set.instHasSubset	—	HasBasis.tendsto_right_iff hasBasis_smallSets

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_basis_of_smallSets 📖	—	Filter.Eventually Set Filter.smallSets Filter.HasBasis	—	—	Set.Subset.rfl Filter.HasBasis.eventually_iff Filter.HasBasis.smallSets
exists_mem_of_smallSets 📖	mathematical	Filter.Eventually Set Filter.smallSets	Filter Filter.instMembership	—	exists_mem_basis_of_smallSets Filter.basis_sets
of_smallSets 📖	—	Filter.Eventually Set Filter.smallSets	—	—	Filter.eventually_smallSets_forall
smallSets 📖	mathematical	Filter.Eventually	Set Filter.smallSets	—	Filter.eventually_smallSets_forall

Filter.Frequently

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smallSets_of_forall_mem_basis 📖	mathematical	Filter.HasBasis	Filter.Frequently Set Filter.smallSets	—	Filter.HasBasis.frequently_iff Filter.HasBasis.smallSets Set.Subset.rfl

Filter.HasAntitoneBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_smallSets 📖	mathematical	Filter.HasAntitoneBasis	Filter.Tendsto Set Filter.atTop Filter.smallSets	—	Filter.tendsto_smallSets_iff eventually_subset

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_smallSets 📖	mathematical	Filter.HasBasis	Filter.Eventually Set Filter.smallSets	—	Filter.eventually_smallSets' exists_iff
frequently_smallSets 📖	mathematical	Filter.HasBasis	Filter.Frequently Set Filter.smallSets	—	Filter.frequently_smallSets' forall_iff
smallSets 📖	mathematical	Filter.HasBasis	Set Filter.smallSets Set.powerset	—	lift' Set.monotone_powerset

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_smallSets 📖	mathematical	Filter.Tendsto	Set Set.image Filter.smallSets	—	Filter.tendsto_image_smallSets
of_smallSets 📖	—	Filter.Tendsto Set Filter.smallSets Filter.Eventually Set.instMembership	—	—	Filter.Eventually.mp Filter.Eventually.mono Filter.tendsto_smallSets_iff
smallSets_mono 📖	—	Filter.Tendsto Set Filter.smallSets Filter.Eventually Set.instHasSubset	—	—	Filter.tendsto_smallSets_iff Filter.Eventually.mp Filter.Eventually.mono HasSubset.Subset.trans Set.instIsTransSubset

---

← Back to Index