mathlib3 documentation

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 α) (h : bornology.cobounded α = bornology.cobounded α) :

x = y

@[ext, class]

structure bornology (α : Type u_4) :

Type u_4

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 of this typeclass

Instances of other typeclasses for bornology

bornology.has_sizeof_inst

theorem bornology.ext_iff {α : Type u_4} (x y : bornology α) :

x = y ↔ bornology.cobounded α = bornology.cobounded α

@[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) :

(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₂ ∈ 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

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 := _}

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

bornology.of_bounded' B empty_mem subset_mem union_mem sUnion_univ = bornology.of_bounded B 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) :

(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

bornology.is_cobounded s = (s ∈ bornology.cobounded α)

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

bornology.is_bounded s = bornology.is_cobounded sᶜ

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

bornology.is_cobounded s ↔ s ∈ bornology.cobounded α

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

bornology.is_bounded s ↔ sᶜ ∈ bornology.cobounded α

@[simp]

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

bornology.is_bounded sᶜ ↔ bornology.is_cobounded s

@[simp]

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

bornology.is_cobounded sᶜ ↔ bornology.is_bounded s

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

bornology.is_bounded sᶜ → bornology.is_cobounded s

Alias of the forward direction of bornology.is_bounded_compl_iff.

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

bornology.is_cobounded s → bornology.is_bounded sᶜ

Alias of the reverse direction of bornology.is_bounded_compl_iff.

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

bornology.is_cobounded sᶜ → bornology.is_bounded s

Alias of the forward direction of bornology.is_cobounded_compl_iff.

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

bornology.is_bounded s → bornology.is_cobounded sᶜ

Alias of the reverse direction of bornology.is_cobounded_compl_iff.

@[simp]

theorem bornology.is_bounded_empty {α : Type u_2} [bornology α] :

bornology.is_bounded ∅

@[simp]

theorem bornology.is_bounded_singleton {α : Type u_2} [bornology α] {x : α} :

bornology.is_bounded {x}

@[simp]

theorem bornology.is_cobounded_univ {α : Type u_2} [bornology α] :

bornology.is_cobounded set.univ

@[simp]

theorem bornology.is_cobounded_inter {α : Type u_2} [bornology α] {s t : set α} :

bornology.is_cobounded (s ∩ t) ↔ bornology.is_cobounded s ∧ bornology.is_cobounded t

theorem bornology.is_cobounded.inter {α : Type u_2} [bornology α] {s t : set α} (hs : bornology.is_cobounded s) (ht : bornology.is_cobounded t) :

bornology.is_cobounded (s ∩ t)

@[simp]

theorem bornology.is_bounded_union {α : Type u_2} [bornology α] {s t : set α} :

bornology.is_bounded (s ∪ t) ↔ bornology.is_bounded s ∧ bornology.is_bounded t

theorem bornology.is_bounded.union {α : Type u_2} [bornology α] {s t : set α} (hs : bornology.is_bounded s) (ht : bornology.is_bounded t) :

bornology.is_bounded (s ∪ t)

theorem bornology.is_cobounded.superset {α : Type u_2} [bornology α] {s t : set α} (hs : bornology.is_cobounded s) (ht : s ⊆ t) :

bornology.is_cobounded t

theorem bornology.is_bounded.subset {α : Type u_2} [bornology α] {s t : set α} (ht : bornology.is_bounded t) (hs : s ⊆ t) :

bornology.is_bounded s

@[simp]

theorem bornology.sUnion_bounded_univ {α : Type u_2} [bornology α] :

⋃₀ {s : set α | bornology.is_bounded s} = set.univ

theorem bornology.comap_cobounded_le_iff {α : Type u_2} {β : Type u_3} [bornology α] [bornology β] {f : α → β} :

filter.comap f (bornology.cobounded β) ≤ bornology.cobounded α ↔ ∀ ⦃s : set α⦄, bornology.is_bounded s → bornology.is_bounded (f '' s)

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 α} :

t = t' ↔ ∀ (s : set α), bornology.is_bounded s ↔ bornology.is_bounded s

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} :

bornology.is_cobounded s ↔ sᶜ ∈ 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} :

bornology.is_bounded s ↔ 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 → bornology.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 ∈ s → bornology.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) :

bornology.is_cobounded (⋂₀ S) ↔ ∀ (s : set α), s ∈ S → bornology.is_cobounded 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) :

bornology.is_bounded (⋃₀ S) ↔ ∀ (s : set α), s ∈ S → bornology.is_bounded 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) :

bornology.is_bounded s

@[protected, instance]

def punit.bornology :

bornology punit

Equations

punit.bornology = {cobounded := ⊥, le_cofinite := punit.bornology._proof_1}

@[reducible]

def bornology.cofinite {α : Type u_2} :

The cofinite filter as a bornology

Equations

bornology.cofinite = {cobounded := filter.cofinite α, le_cofinite := _}

@[class]

structure bounded_space (α : Type u_4) [bornology α] :

Prop

bounded_univ : bornology.is_bounded set.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 α] :

bornology.is_bounded set.univ ↔ bounded_space α

theorem bornology.cobounded_eq_bot_iff {α : Type u_2} [bornology α] :

bornology.cobounded α = ⊥ ↔ bounded_space α

theorem bornology.is_bounded.all {α : Type u_2} [bornology α] [bounded_space α] (s : set α) :

bornology.is_bounded s

theorem bornology.is_cobounded.all {α : Type u_2} [bornology α] [bounded_space α] (s : set α) :

bornology.is_cobounded s

@[simp]

theorem bornology.cobounded_eq_bot (α : Type u_2) [bornology α] [bounded_space α] :

bornology.cobounded α = ⊥