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.of_bounded
,
is_bounded.union
, is_bounded.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.is_cobounded
: the predicate that a set is a member of thecobounded α
filter. Fors : set α
, one should preferbornology.is_cobounded s
overs ∈ cobounded α
.bornology.is_bounded
: the predicate that states a set is bounded (i.e., the complement of a cobounded set). One should preferbornology.is_bounded s
oversᶜ ∈ cobounded α
.bounded_space α
: a class extendingbornology α
with the conditionbornology.is_bounded (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 α
.
- cobounded : filter α
- le_cofinite : bornology.cobounded α ≤ filter.cofinite
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.of_bounded
and bornology.ext_iff_is_bounded
Instances
A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.
Equations
- bornology.of_bounded B empty_mem subset_mem union_mem singleton_mem = {cobounded := {sets := {s : set α | sᶜ ∈ B}, univ_sets := _, sets_of_superset := _, inter_sets := _}, le_cofinite := _}
A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.
Equations
- bornology.of_bounded' B empty_mem subset_mem union_mem sUnion_univ = bornology.of_bounded B empty_mem subset_mem union_mem _
is_cobounded
is the predicate that s
is in the filter of cobounded sets in the ambient
bornology on α
Equations
- bornology.is_cobounded s = (s ∈ bornology.cobounded α)
is_bounded
is the predicate that s
is bounded relative to the ambient bornology on α
.
Equations
Alias of is_bounded_compl_iff
.
Alias of is_bounded_compl_iff
.
Alias of is_cobounded_compl_iff
.
Alias of is_cobounded_compl_iff
.
Equations
- punit.bornology = {cobounded := ⊥, le_cofinite := punit.bornology._proof_1}
The cofinite filter as a bornology
Equations
- bornology.cofinite = {cobounded := filter.cofinite α, le_cofinite := _}