Basic theory of bornology #
We develop the basic theory of bornologies. Instead of axiomatizing bounded sets and defining bornologies in terms of those, we recognize that the cobounded sets form a filter and define a bornology as a filter of cobounded sets which contains the cofinite filter. This allows us to make use of the extensive library for filters, but we also provide the relevant connecting results for bounded sets.
The specification of a bornology in terms of the cobounded filter is equivalent to the standard
one (e.g., see Bourbaki, Topological Vector Spaces, covering bornology, now
often called simply bornology) in terms of bounded sets (see Bornology.ofBounded
,
IsBounded.union
, IsBounded.subset
), except that we do not allow the empty bornology (that is,
we require that some set must be bounded; equivalently, ∅
is bounded). In the literature the
cobounded filter is generally referred to as the filter at infinity.
Main definitions #
Bornology α
: a class consisting ofcobounded : Filter α
and a proof that this filter contains thecofinite
filter.Bornology.IsCobounded
: the predicate that a set is a member of thecobounded α
filter. Fors : Set α
, one should preferBornology.IsCobounded s
overs ∈ cobounded α
.bornology.IsBounded
: the predicate that states a set is bounded (i.e., the complement of a cobounded set). One should preferBornology.IsBounded s
oversᶜ ∈ cobounded α
.BoundedSpace α
: a class extendingBornology α
with the conditionBornology.IsBounded (Set.univ : Set α)
Although use of cobounded α
is discouraged for indicating the (co)boundedness of individual sets,
it is intended for regular use as a filter on α
.
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
- cobounded' : Filter α
The filter of cobounded sets in a bornology. This is a field of the structure, but one should always prefer
Bornology.cobounded
because it makes theα
argument explicit. - le_cofinite' : Bornology.cobounded' ≤ Filter.cofinite
The cobounded filter in a bornology is smaller than the cofinite filter. This is a field of the structure, but one should always prefer
Bornology.le_cofinite
because it makes theα
argument explicit.
Instances
The filter of cobounded sets in a bornology.
Equations
- Bornology.cobounded α = Bornology.cobounded'
Instances For
A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.
Equations
- Bornology.ofBounded B empty_mem subset_mem union_mem singleton_mem = { cobounded' := Filter.comk (fun (x : Set α) => x ∈ B) empty_mem subset_mem union_mem, le_cofinite' := ⋯ }
Instances For
A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.
Equations
- Bornology.ofBounded' B empty_mem subset_mem union_mem sUnion_univ = Bornology.ofBounded B empty_mem subset_mem union_mem ⋯
Instances For
IsCobounded
is the predicate that s
is in the filter of cobounded sets in the ambient
bornology on α
Equations
- Bornology.IsCobounded s = (s ∈ Bornology.cobounded α)
Instances For
IsBounded
is the predicate that s
is bounded relative to the ambient bornology on α
.
Equations
Instances For
Alias of the forward direction of Bornology.isBounded_compl_iff
.
Alias of the reverse direction of Bornology.isBounded_compl_iff
.
Alias of the forward direction of Bornology.isCobounded_compl_iff
.
Alias of the reverse direction of Bornology.isCobounded_compl_iff
.
Equations
- instBornologyPUnit = { cobounded' := ⊥, le_cofinite' := instBornologyPUnit.proof_1 }
The cofinite filter as a bornology
Equations
- Bornology.cofinite = { cobounded' := Filter.cofinite, le_cofinite' := ⋯ }
Instances For
A space with a Bornology
is a bounded space if Set.univ : Set α
is bounded.
- bounded_univ : Bornology.IsBounded Set.univ
The
Set.univ
is bounded.
Instances
A finite space is bounded.