Mathlib Map

Theorems · Definition · general topology

Bornology.IsCobounded

{α : Type u_2} → [Bornology α] → Set α → Prop

IsCobounded is the predicate that s is in the filter of cobounded sets in the ambient bornology on α

Defined in
Mathlib.Topology.Bornology.Basic
Cited by
23 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Assumes
Bornology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Bornology.IsBounded · cited by 293Bornology.IsBoundedBornology.isBounded_compl_iff · cited by 8Bornology.isBounded_compl…Bornology.isCobounded_def · cited by 4Bornology.isCobounded_defBornology.isBounded_biUnion · cited by 3Bornology.isBounded_biUni…Bornology.isCobounded_compl_iff · cited by 2Bornology.isCobounded_com…Bornology.IsBounded.compl · cited by 2IsBounded.complBornology.isBounded_union · cited by 1Bornology.isBounded_unionBornology.isCobounded_biInter · cited by 1Bornology.isCobounded_biI…Bornology.isCobounded_inter · cited by 1Bornology.isCobounded_int…Bornology.IsCobounded.closedBall_compl_subset · cited by 1IsCobounded.closedBall_co…Bornology.IsCobounded.compl · cited by 1IsCobounded.complBornology.IsCobounded.superset · cited by 1IsCobounded.supersetMetric.isCobounded_iff_closedBall_compl_subset · cited by 1Metric.isCobounded_iff_cl…Bornology.isCobounded_biInter_finset · cited by 0Bornology.isCobounded_biI…Bornology.isCobounded_iInter · cited by 0Bornology.isCobounded_iIn…Set · cited by 53352SetBornology · cited by 188BornologyBornology.cobounded · cited by 162Bornology.coboundedBornology.IsCoboundedCITED BYCITES

Cites3

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

Cited by24

Results whose statement or proof uses this declaration.