# mathlib3documentation

topology.bornology.basic

# Basic theory of bornology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 of cobounded : filter α and a proof that this filter contains the cofinite filter.
• bornology.is_cobounded: the predicate that a set is a member of the cobounded α filter. For s : set α, one should prefer bornology.is_cobounded s over s ∈ cobounded α.
• bornology.is_bounded: the predicate that states a set is bounded (i.e., the complement of a cobounded set). One should prefer bornology.is_bounded s over sᶜ ∈ cobounded α.
• bounded_space α: a class extending bornology α with the condition bornology.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 α.

theorem bornology.ext {α : Type u_4} (x y : bornology α)  :
x = y
@[ext, class]
structure bornology (α : Type u_4) :
Type u_4
• cobounded :
• le_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 of this typeclass
Instances of other typeclasses for bornology
• bornology.has_sizeof_inst
theorem bornology.ext_iff {α : Type u_4} (x y : bornology α) :
@[simp]
theorem bornology.of_bounded_cobounded_sets {α : Type u_1} (B : set (set α)) (empty_mem : B) (subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B) (union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B) (singleton_mem : (x : α), {x} B) :
= {s : set α | s B}
def bornology.of_bounded {α : Type u_1} (B : set (set α)) (empty_mem : B) (subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B) (union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B) (singleton_mem : (x : α), {x} B) :

A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.

Equations
def bornology.of_bounded' {α : Type u_1} (B : set (set α)) (empty_mem : B) (subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B) (union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B) (sUnion_univ : ⋃₀ B = set.univ) :

A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.

Equations
• empty_mem subset_mem union_mem sUnion_univ = empty_mem subset_mem union_mem _
@[simp]
theorem bornology.of_bounded'_cobounded_sets {α : Type u_1} (B : set (set α)) (empty_mem : B) (subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B) (union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B) (sUnion_univ : ⋃₀ B = set.univ) :
= {s : set α | s B}
def bornology.is_cobounded {α : Type u_2} [bornology α] (s : set α) :
Prop

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

Equations
def bornology.is_bounded {α : Type u_2} [bornology α] (s : set α) :
Prop

is_bounded is the predicate that s is bounded relative to the ambient bornology on α.

Equations
theorem bornology.is_cobounded_def {α : Type u_2} [bornology α] {s : set α} :
theorem bornology.is_bounded_def {α : Type u_2} [bornology α] {s : set α} :
@[simp]
theorem bornology.is_bounded_compl_iff {α : Type u_2} [bornology α] {s : set α} :
@[simp]
theorem bornology.is_cobounded_compl_iff {α : Type u_2} [bornology α] {s : set α} :
theorem bornology.is_bounded.of_compl {α : Type u_2} [bornology α] {s : set α} :

Alias of the forward direction of bornology.is_bounded_compl_iff.

theorem bornology.is_cobounded.compl {α : Type u_2} [bornology α] {s : set α} :

Alias of the reverse direction of bornology.is_bounded_compl_iff.

theorem bornology.is_cobounded.of_compl {α : Type u_2} [bornology α] {s : set α} :

Alias of the forward direction of bornology.is_cobounded_compl_iff.

theorem bornology.is_bounded.compl {α : Type u_2} [bornology α] {s : set α} :

Alias of the reverse direction of bornology.is_cobounded_compl_iff.

@[simp]
theorem bornology.is_bounded_empty {α : Type u_2} [bornology α] :
@[simp]
theorem bornology.is_bounded_singleton {α : Type u_2} [bornology α] {x : α} :
@[simp]
theorem bornology.is_cobounded_univ {α : Type u_2} [bornology α] :
@[simp]
theorem bornology.is_cobounded_inter {α : Type u_2} [bornology α] {s t : set α} :
@[simp]
theorem bornology.is_bounded_union {α : Type u_2} [bornology α] {s t : set α} :
theorem bornology.is_cobounded.superset {α : Type u_2} [bornology α] {s t : set α} (hs : bornology.is_cobounded s) (ht : s t) :
theorem bornology.is_bounded.subset {α : Type u_2} [bornology α] {s t : set α} (ht : bornology.is_bounded t) (hs : s t) :
@[simp]
theorem bornology.sUnion_bounded_univ {α : Type u_2} [bornology α] :
⋃₀ {s : set α | = set.univ
theorem bornology.comap_cobounded_le_iff {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f : α β} :
⦃s : set α⦄,
theorem bornology.ext_iff' {α : Type u_2} {t t' : bornology α} :
t = t' (s : set α), s s
theorem bornology.ext_iff_is_bounded {α : Type u_2} {t t' : bornology α} :
t = t' (s : set α),
theorem bornology.is_cobounded_of_bounded_iff {α : Type u_2} {s : set α} (B : set (set α)) {empty_mem : B} {subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B} {union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B} {sUnion_univ : (x : α), {x} B} :
theorem bornology.is_bounded_of_bounded_iff {α : Type u_2} {s : set α} (B : set (set α)) {empty_mem : B} {subset_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ s₁ s₂ B} {union_mem : (s₁ : set α), s₁ B (s₂ : set α), s₂ B s₁ s₂ B} {sUnion_univ : (x : α), {x} B} :
s B
theorem bornology.is_cobounded_bInter {ι : Type u_1} {α : Type u_2} [bornology α] {s : set ι} {f : ι set α} (hs : s.finite) :
bornology.is_cobounded ( (i : ι) (H : i s), f i) (i : ι), i s
@[simp]
theorem bornology.is_cobounded_bInter_finset {ι : Type u_1} {α : Type u_2} [bornology α] (s : finset ι) {f : ι set α} :
bornology.is_cobounded ( (i : ι) (H : i s), f i) (i : ι), i s
@[simp]
theorem bornology.is_cobounded_Inter {ι : Type u_1} {α : Type u_2} [bornology α] [finite ι] {f : ι set α} :
bornology.is_cobounded ( (i : ι), f i) (i : ι),
theorem bornology.is_cobounded_sInter {α : Type u_2} [bornology α] {S : set (set α)} (hs : S.finite) :
(s : set α), s S
theorem bornology.is_bounded_bUnion {ι : Type u_1} {α : Type u_2} [bornology α] {s : set ι} {f : ι set α} (hs : s.finite) :
bornology.is_bounded ( (i : ι) (H : i s), f i) (i : ι), i s bornology.is_bounded (f i)
theorem bornology.is_bounded_bUnion_finset {ι : Type u_1} {α : Type u_2} [bornology α] (s : finset ι) {f : ι set α} :
bornology.is_bounded ( (i : ι) (H : i s), f i) (i : ι), i s bornology.is_bounded (f i)
theorem bornology.is_bounded_sUnion {α : Type u_2} [bornology α] {S : set (set α)} (hs : S.finite) :
(s : set α), s S
@[simp]
theorem bornology.is_bounded_Union {ι : Type u_1} {α : Type u_2} [bornology α] [finite ι] {s : ι set α} :
bornology.is_bounded ( (i : ι), s i) (i : ι), bornology.is_bounded (s i)
theorem set.finite.is_bounded {α : Type u_2} [bornology α] {s : set α} (hs : s.finite) :
@[protected, instance]
Equations
@[reducible]
def bornology.cofinite {α : Type u_2} :

The cofinite filter as a bornology

Equations
@[class]
structure bounded_space (α : Type u_4) [bornology α] :
Prop
• bounded_univ :

A space with a bornology is a bounded space if set.univ : set α is bounded.

Instances of this typeclass
theorem bornology.is_bounded_univ {α : Type u_2} [bornology α] :
theorem bornology.is_bounded.all {α : Type u_2} [bornology α] (s : set α) :
theorem bornology.is_cobounded.all {α : Type u_2} [bornology α] (s : set α) :
@[simp]
theorem bornology.cobounded_eq_bot (α : Type u_2) [bornology α]  :