Structures · Topology
Bornology
A bornology on a type α is a filter of cobounded sets which contains the cofinite filter.
Such spaces are equivalently specified by their bounded sets, see Bornology.ofBounded
and Bornology.ext_iff_isBounded
- Defined in
- Mathlib.Topology.Bornology.Basic
- Shape
- One type argument · adds cobounded, le_cofinite
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances14
- CStarMatrix
- Unitization
- WithLp
- WithCStarModule
- PiLp
- WeakDual
- Metric.Snowflaking
- Born.carrier
- Subtype
- Prod
- OrderDual
- PUnit
- Multiplicative
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by183
- Bornology.IsBounded
- Bornology.cobounded
- Absorbent
- Absorbs
- Bornology.IsCobounded
- Bornology.IsBounded.bddBelow
- LocallyBoundedMap.comp
- Bornology.IsBounded.bddAbove
- isBounded_iff_bddBelow_bddAbove
- Absorbent.mono
- Absorbs.mono_right
- Bornology.eventually_ne_cobounded
- Bornology.isBounded_univ
- Bornology.induced
- IsOrderBornology.cobounded_eq
- Absorbs.mono_left
- Set.Finite.isBounded
- LocallyBoundedMap.id
- IsOrderBornology.atTop_le_cobounded
- Absorbs.add
- Bornology.isBounded_induced
- Bornology.isBounded_biUnion
- isBounded_add
- Bornology.forall_isBounded_image_eval_iff
- Set.Finite.absorbs_biUnion
- Absorbent.absorbs
- Bornology.IsBounded.prod
- Bornology.IsBounded.subset_Icc_sInf_sSup
- Bornology.isBounded_image_fst_and_snd
- Filter.absorbing
- Bornology.le_cofinite
- Metric.Snowflaking.isBounded_image_ofSnowflaking_iff
- isBounded_mul
- Absorbs.neg_neg
- boundedSpace_subtype_iff
- IsOrderBornology.atBot_le_cobounded
- Bornology.cobounded_eq_bot_iff
- boundedSpace_val_set_iff
- LocallyBoundedMap.ofMapBounded
- Bornology.IsBounded.all
- Set.Finite.absorbs_sUnion
- absorbs_neg_neg
- isBounded_sub
- Filter.disjoint_cobounded_iff
- Bornology.isBounded_prod_of_nonempty
- Bornology.cobounded_eq_bot
- LocallyBoundedMap.copy
- absorbs_iff_eventually_cobounded_mapsTo
- Bornology.IsBounded.image
- Absorbs.empty
Ancestors0
No ancestors.