Mathlib Map

Theorems · Definition · general topology

Bornology.cobounded

(α : Type u_4) → [self : Bornology α] → Filter α

The filter of cobounded sets in a bornology.

Defined in
Mathlib.Topology.Bornology.Basic
Cited by
162 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Assumes
Bornology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Absorbs · cited by 59AbsorbsBornology.IsCobounded · cited by 23Bornology.IsCoboundedtendsto_norm_atTop_iff_cobounded · cited by 13tendsto_norm_atTop_iff_co…tendsto_norm_cobounded_atTop · cited by 11tendsto_norm_cobounded_at…Bornology.isBounded_def · cited by 9Bornology.isBounded_defBornology.isBounded_compl_iff · cited by 8Bornology.isBounded_compl…Metric.cobounded_eq_cocompact · cited by 8Metric.cobounded_eq_cocom…Metric.disjoint_nhds_cobounded · cited by 7Metric.disjoint_nhds_cobo…Bornology.eventually_ne_cobounded · cited by 6Bornology.eventually_ne_c…Filter.tendsto_inv₀_cobounded · cited by 6Filter.tendsto_inv₀_cobou…PseudoMetricSpace.ext · cited by 6PseudoMetricSpace.extBornology.induced · cited by 5Bornology.inducedBornology.isBounded_empty · cited by 5Bornology.isBounded_emptyPhragmenLindelof.isBigO_sub_exp_rpow · cited by 5PhragmenLindelof.isBigO_s…tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded · cited by 5tendsto_zero_of_isBounded…Filter · cited by 8121FilterBornology · cited by 188BornologyBornology.coboundedCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Filterstatement · cited by 8,121
  • Bornologystatement and proof · cited by 188

Cited by177

Results whose statement or proof uses this declaration.