mathlib documentation

topology.bornology.basic

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 #

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 α) (h : bornology.cobounded α = bornology.cobounded α) :
x = y
@[ext, class]
structure bornology (α : Type u_4) :
Type u_4

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₂ Bs₁ s₂ B) (singleton_mem : ∀ (x : α), {x} B) :
(bornology.cobounded α).sets = {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₂ Bs₁ 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₂ Bs₁ 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
@[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₂ Bs₁ s₂ B) (sUnion_univ : ⋃₀ B = set.univ) :
(bornology.cobounded α).sets = {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

Alias of the forward direction of bornology.is_bounded_compl_iff.

Alias of the reverse direction of bornology.is_bounded_compl_iff.

Alias of the forward direction of bornology.is_cobounded_compl_iff.

Alias of the reverse direction of bornology.is_cobounded_compl_iff.

@[simp]
@[simp]
theorem bornology.is_bounded_singleton {α : Type u_2} [bornology α] {x : α} :
theorem bornology.is_bounded.union {α : Type u_2} [bornology α] {s t : set α} (hs : bornology.is_bounded s) (ht : bornology.is_bounded t) :
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 α] :
theorem bornology.comap_cobounded_le_iff {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f : α → β} :
theorem bornology.ext_iff' {α : Type u_2} {t t' : bornology α} :
t = t' ∀ (s : set α), (bornology.cobounded α).sets s (bornology.cobounded α).sets s
theorem bornology.ext_iff_is_bounded {α : Type u_2} {t t' : bornology α} :
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₂ Bs₁ 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₂ Bs₁ s₂ B} {sUnion_univ : ∀ (x : α), {x} 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 sbornology.is_cobounded (f i)
@[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 sbornology.is_cobounded (f i)
@[simp]
theorem bornology.is_cobounded_Inter {ι : Type u_1} {α : Type u_2} [bornology α] [finite ι] {f : ι → set α} :
bornology.is_cobounded (⋂ (i : ι), f i) ∀ (i : ι), bornology.is_cobounded (f i)
theorem bornology.is_cobounded_sInter {α : Type u_2} [bornology α] {S : set (set α)} (hs : S.finite) :
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 sbornology.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 sbornology.is_bounded (f i)
theorem bornology.is_bounded_sUnion {α : Type u_2} [bornology α] {S : set (set α)} (hs : S.finite) :
@[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

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

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