Documentation

Mathlib.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][bourbaki1987], 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 of cobounded : Filter α and a proof that this filter contains the cofinite filter.
Bornology.IsCobounded: the predicate that a set is a member of the cobounded α filter. For s : set α, one should prefer Bornology.IsCobounded s over s ∈ cobounded α∈ cobounded α.
bornology.IsBounded: the predicate that states a set is bounded (i.e., the complement of a cobounded set). One should prefer Bornology.IsBounded s over sᶜ ∈ cobounded α∈ cobounded α.
BoundedSpace α: a class extending Bornology α with the condition Bornology.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 α.

class Bornology (α : Type u_1) :

Type u_1

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 explciit.
cobounded' : Filter α
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 explciit.
le_cofinite' : 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.ofBounded and Bornology.ext_iff_isBounded

Instances

def Bornology.cobounded (α : Type u_1) [inst : Bornology α] :

The filter of cobounded sets in a bornology.

Equations

Bornology.cobounded α = Bornology.cobounded'

def Bornology.Simps.cobounded (α : Type u_1) [inst : Bornology α] :

Alias of Bornology.cobounded.

Equations

Bornology.Simps.cobounded = Bornology.cobounded

theorem Bornology.le_cofinite (α : Type u_1) [inst : Bornology α] :

Bornology.cobounded α ≤ Filter.cofinite

theorem Bornology.ext {α : Type u_1} (t : Bornology α) (t' : Bornology α) (h_cobounded : Bornology.cobounded α = Bornology.cobounded α) :

t = t'

theorem Bornology.ext_iff {α : Type u_1} (t : Bornology α) (t' : Bornology α) :

t = t' ↔ Bornology.cobounded α = Bornology.cobounded α

@[simp]

theorem Bornology.ofBounded_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 | sᶜ ∈ B }

def Bornology.ofBounded {α : 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

One or more equations did not get rendered due to their size.

@[simp]

theorem Bornology.ofBounded'_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) (unionₛ_univ : ⋃₀ B = Set.univ) :

(Bornology.cobounded α).sets = { s | sᶜ ∈ B }

def Bornology.ofBounded' {α : 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) (unionₛ_univ : ⋃₀ B = Set.univ) :

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 unionₛ_univ = Bornology.ofBounded B empty_mem subset_mem union_mem (_ : ∀ (x : α), {x} ∈ B)

def Bornology.IsCobounded {α : Type u_1} [inst : Bornology α] (s : Set α) :

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 α)

def Bornology.IsBounded {α : Type u_1} [inst : Bornology α] (s : Set α) :

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

Equations

Bornology.IsBounded s = Bornology.IsCobounded (sᶜ)

theorem Bornology.isCobounded_def {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsCobounded s ↔ s ∈ Bornology.cobounded α

theorem Bornology.isBounded_def {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsBounded s ↔ sᶜ ∈ Bornology.cobounded α

@[simp]

theorem Bornology.isBounded_compl_iff {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsBounded (sᶜ) ↔ Bornology.IsCobounded s

@[simp]

theorem Bornology.isCobounded_compl_iff {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsCobounded (sᶜ) ↔ Bornology.IsBounded s

theorem Bornology.IsBounded.of_compl {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsBounded (sᶜ) → Bornology.IsCobounded s

Alias of the forward direction of Bornology.isBounded_compl_iff.

theorem Bornology.IsCobounded.compl {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsCobounded s → Bornology.IsBounded (sᶜ)

Alias of the reverse direction of Bornology.isBounded_compl_iff.

theorem Bornology.IsBounded.compl {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsBounded s → Bornology.IsCobounded (sᶜ)

Alias of the reverse direction of Bornology.isCobounded_compl_iff.

theorem Bornology.IsCobounded.of_compl {α : Type u_1} [inst : Bornology α] {s : Set α} :

Bornology.IsCobounded (sᶜ) → Bornology.IsBounded s

Alias of the forward direction of Bornology.isCobounded_compl_iff.

@[simp]

theorem Bornology.isBounded_empty {α : Type u_1} [inst : Bornology α] :

Bornology.IsBounded ∅

@[simp]

theorem Bornology.isBounded_singleton {α : Type u_1} [inst : Bornology α] {x : α} :

Bornology.IsBounded {x}

@[simp]

theorem Bornology.isCobounded_univ {α : Type u_1} [inst : Bornology α] :

Bornology.IsCobounded Set.univ

@[simp]

theorem Bornology.isCobounded_inter {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} :

Bornology.IsCobounded (s ∩ t) ↔ Bornology.IsCobounded s ∧ Bornology.IsCobounded t

theorem Bornology.IsCobounded.inter {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} (hs : Bornology.IsCobounded s) (ht : Bornology.IsCobounded t) :

Bornology.IsCobounded (s ∩ t)

@[simp]

theorem Bornology.isBounded_union {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} :

Bornology.IsBounded (s ∪ t) ↔ Bornology.IsBounded s ∧ Bornology.IsBounded t

theorem Bornology.IsBounded.union {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) :

Bornology.IsBounded (s ∪ t)

theorem Bornology.IsCobounded.superset {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} (hs : Bornology.IsCobounded s) (ht : s ⊆ t) :

Bornology.IsCobounded t

theorem Bornology.IsBounded.subset {α : Type u_1} [inst : Bornology α] {s : Set α} {t : Set α} (ht : Bornology.IsBounded t) (hs : s ⊆ t) :

Bornology.IsBounded s

@[simp]

theorem Bornology.unionₛ_bounded_univ {α : Type u_1} [inst : Bornology α] :

⋃₀ { s | Bornology.IsBounded s } = Set.univ

theorem Bornology.comap_cobounded_le_iff {α : Type u_2} {β : Type u_1} [inst : Bornology α] [inst : Bornology β] {f : α → β} :

Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α ↔ ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)

theorem Bornology.ext_iff' {α : Type u_1} {t : Bornology α} {t' : Bornology α} :

t = t' ↔ ∀ (s : Set α), Filter.sets (Bornology.cobounded α) s ↔ Filter.sets (Bornology.cobounded α) s

theorem Bornology.ext_iff_isBounded {α : Type u_1} {t : Bornology α} {t' : Bornology α} :

t = t' ↔ ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s

theorem Bornology.isCobounded_ofBounded_iff {α : Type u_1} {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.IsCobounded s ↔ sᶜ ∈ B

theorem Bornology.isBounded_ofBounded_iff {α : Type u_1} {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.IsBounded s ↔ s ∈ B

theorem Bornology.isCobounded_binterᵢ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α} (hs : Set.Finite s) :

Bornology.IsCobounded (Set.interᵢ fun i => Set.interᵢ fun h => f i) ↔ ∀ (i : ι), i ∈ s → Bornology.IsCobounded (f i)

@[simp]

theorem Bornology.isCobounded_binterᵢ_finset {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α} :

Bornology.IsCobounded (Set.interᵢ fun i => Set.interᵢ fun h => f i) ↔ ∀ (i : ι), i ∈ s → Bornology.IsCobounded (f i)

@[simp]

theorem Bornology.isCobounded_interᵢ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst : Finite ι] {f : ι → Set α} :

Bornology.IsCobounded (Set.interᵢ fun i => f i) ↔ ∀ (i : ι), Bornology.IsCobounded (f i)

theorem Bornology.isCobounded_interₛ {α : Type u_1} [inst : Bornology α] {S : Set (Set α)} (hs : Set.Finite S) :

Bornology.IsCobounded (⋂₀ S) ↔ ∀ (s : Set α), s ∈ S → Bornology.IsCobounded s

theorem Bornology.isBounded_bunionᵢ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α} (hs : Set.Finite s) :

Bornology.IsBounded (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) ↔ ∀ (i : ι), i ∈ s → Bornology.IsBounded (f i)

theorem Bornology.isBounded_bunionᵢ_finset {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α} :

Bornology.IsBounded (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) ↔ ∀ (i : ι), i ∈ s → Bornology.IsBounded (f i)

theorem Bornology.isBounded_unionₛ {α : Type u_1} [inst : Bornology α] {S : Set (Set α)} (hs : Set.Finite S) :

Bornology.IsBounded (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → Bornology.IsBounded s

@[simp]

theorem Bornology.isBounded_unionᵢ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] [inst : Finite ι] {s : ι → Set α} :

Bornology.IsBounded (Set.unionᵢ fun i => s i) ↔ ∀ (i : ι), Bornology.IsBounded (s i)

theorem Set.Finite.isBounded {α : Type u_1} [inst : Bornology α] {s : Set α} (hs : Set.Finite s) :

Bornology.IsBounded s

instance instBornologyPUnit :

Bornology PUnit

Equations

instBornologyPUnit = { cobounded' := ⊥, le_cofinite' := instBornologyPUnit.proof_1 }

def Bornology.cofinite {α : Type u_1} :

The cofinite filter as a bornology

Equations

Bornology.cofinite = { cobounded' := Filter.cofinite, le_cofinite' := (_ : Filter.cofinite ≤ Filter.cofinite) }

class BoundedSpace (α : Type u_1) [inst : Bornology α] :

The Set.univ is bounded.
bounded_univ : Bornology.IsBounded Set.univ

A space with a Bornology is a bounded space if Set.univ : Set α is bounded.

Instances

theorem Bornology.isBounded_univ {α : Type u_1} [inst : Bornology α] :

Bornology.IsBounded Set.univ ↔ BoundedSpace α

theorem Bornology.cobounded_eq_bot_iff {α : Type u_1} [inst : Bornology α] :

Bornology.cobounded α = ⊥ ↔ BoundedSpace α

theorem Bornology.IsBounded.all {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] (s : Set α) :

Bornology.IsBounded s

theorem Bornology.IsCobounded.all {α : Type u_1} [inst : Bornology α] [inst : BoundedSpace α] (s : Set α) :

Bornology.IsCobounded s

@[simp]

theorem Bornology.cobounded_eq_bot (α : Type u_1) [inst : Bornology α] [inst : BoundedSpace α] :

Bornology.cobounded α = ⊥