Mathlib.Topology.Bornology.Basic

Bornology structure

(α : Type*)

Full source

/-- 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` -/
class Bornology (α : Type*) where
  /-- 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 explicit. -/
  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 explicit. -/
  le_cofinite' : cobounded' ≤ cofinite

Bornology

Informal description

A bornology on a type $\alpha$ is a structure consisting of a filter of cobounded sets (sets with bounded complement) that contains the cofinite filter. This provides an alternative characterization of bornologies compared to the traditional definition in terms of bounded sets, while ensuring that at least some sets are bounded (in particular, the empty set is always bounded).

Bornology.cobounded definition

(α : Type*) [Bornology α] : Filter α

Full source

/-- The filter of cobounded sets in a bornology. -/
def Bornology.cobounded (α : Type*) [Bornology α] : Filter α := Bornology.cobounded'

Filter of cobounded sets in a bornology

Informal description

The filter `cobounded α` on a type `α` equipped with a bornology consists of all cobounded sets, i.e., sets whose complements are bounded. This filter contains the cofinite filter (all sets with finite complement) by definition of a bornology.

Bornology.le_cofinite theorem

(α : Type*) [Bornology α] : cobounded α ≤ cofinite

Full source

lemma Bornology.le_cofinite (α : Type*) [Bornology α] : cobounded α ≤ cofinite :=
Bornology.le_cofinite'

Cobounded Filter Contains Cofinite Filter in a Bornology

Informal description

For any type $\alpha$ equipped with a bornology, the filter of cobounded sets is finer than the cofinite filter. In other words, every set with finite complement is cobounded.

Bornology.ext theorem

(t t' : Bornology α) (h_cobounded : @Bornology.cobounded α t = @Bornology.cobounded α t') : t = t'

Full source

@[ext]
lemma Bornology.ext (t t' : Bornology α)
    (h_cobounded : @Bornology.cobounded α t = @Bornology.cobounded α t') :
    t = t' := by
  cases t
  cases t'
  congr

Equality of Bornologies via Cobounded Filters

Informal description

Let $t$ and $t'$ be two bornologies on a type $\alpha$. If their cobounded filters coincide (i.e., $\text{cobounded}_{\alpha} t = \text{cobounded}_{\alpha} t'$), then $t = t'$.

Bornology.ofBounded definition

 {α : Type*} (B : Set (Set α)) (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
  (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (singleton_mem : ∀ x, { x } ∈ B) : Bornology α

Full source

/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps]
def Bornology.ofBounded {α : Type*} (B : Set (Set α))
    (empty_mem : ∅∅ ∈ B)
    (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
    (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B)
    (singleton_mem : ∀ x, {x}{x} ∈ B) : Bornology α where
  cobounded' := comk (· ∈ B) empty_mem subset_mem union_mem
  le_cofinite' := by simpa [le_cofinite_iff_compl_singleton_mem]

Construction of a bornology from bounded sets

Informal description

Given a type $\alpha$ and a collection $B$ of subsets of $\alpha$ satisfying: 1. The empty set is in $B$, 2. Any subset of a set in $B$ is also in $B$ (closure under subsets), 3. The union of any two sets in $B$ is in $B$ (closure under finite unions), 4. Every singleton set $\{x\}$ is in $B$, this constructs a bornology on $\alpha$ where the cobounded sets are exactly those whose complements are in $B$.

Bornology.ofBounded' definition

 {α : Type*} (B : Set (Set α)) (empty_mem : ∅ ∈ B) (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
  (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B) (sUnion_univ : ⋃₀ B = univ) : Bornology α

Full source

/-- A constructor for bornologies by specifying the bounded sets,
and showing that they satisfy the appropriate conditions. -/
@[simps! cobounded]
def Bornology.ofBounded' {α : Type*} (B : Set (Set α))
    (empty_mem : ∅∅ ∈ B)
    (subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B)
    (union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B)
    (sUnion_univ : ⋃₀ B = univ) :
    Bornology α :=
  Bornology.ofBounded B empty_mem subset_mem union_mem fun x => by
    rw [sUnion_eq_univ_iff] at sUnion_univ
    rcases sUnion_univ x with ⟨s, hs, hxs⟩
    exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)

Construction of a bornology from a covering family of bounded sets

Informal description

Given a type $\alpha$ and a collection $B$ of subsets of $\alpha$ satisfying: 1. The empty set is in $B$, 2. Any subset of a set in $B$ is also in $B$ (closure under subsets), 3. The union of any two sets in $B$ is in $B$ (closure under finite unions), 4. The union of all sets in $B$ equals the universal set (i.e., $\bigcup_{s \in B} s = \alpha$), this constructs a bornology on $\alpha$ where the cobounded sets are exactly those whose complements are in $B$.

Bornology.IsCobounded definition

[Bornology α] (s : Set α) : Prop

Full source

/-- `IsCobounded` is the predicate that `s` is in the filter of cobounded sets in the ambient
bornology on `α` -/
def IsCobounded [Bornology α] (s : Set α) : Prop :=
  s ∈ cobounded α

Cobounded set in a bornology

Informal description

Given a bornology on a type $\alpha$, the predicate `IsCobounded s` holds for a set $s \subseteq \alpha$ if and only if $s$ belongs to the filter of cobounded sets, i.e., the complement of $s$ is bounded in the bornology.

Bornology.IsBounded definition

[Bornology α] (s : Set α) : Prop

Full source

/-- `IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`. -/
def IsBounded [Bornology α] (s : Set α) : Prop :=
  IsCobounded sᶜ

Bounded set in a bornology

Informal description

Given a bornology on a type $\alpha$, the predicate `IsBounded s` holds for a set $s \subseteq \alpha$ if and only if the complement of $s$ is cobounded in the bornology, i.e., $s$ is bounded relative to the ambient bornology.

Bornology.isCobounded_def theorem

{s : Set α} : IsCobounded s ↔ s ∈ cobounded α

Full source

theorem isCobounded_def {s : Set α} : IsCoboundedIsCobounded s ↔ s ∈ cobounded α :=
  Iff.rfl

Characterization of Cobounded Sets via Filter Membership

Informal description

For any set $s$ in a type $\alpha$ equipped with a bornology, the predicate $\text{IsCobounded}(s)$ holds if and only if $s$ belongs to the filter of cobounded sets $\text{cobounded}(\alpha)$.

Bornology.isBounded_def theorem

{s : Set α} : IsBounded s ↔ sᶜ ∈ cobounded α

Full source

theorem isBounded_def {s : Set α} : IsBoundedIsBounded s ↔ sᶜ ∈ cobounded α :=
  Iff.rfl

Characterization of Bounded Sets via Cobounded Filter

Informal description

For any set $s$ in a type $\alpha$ equipped with a bornology, $s$ is bounded if and only if its complement $s^c$ belongs to the cobounded filter.

Bornology.isBounded_compl_iff theorem

: IsBounded sᶜ ↔ IsCobounded s

Full source

@[simp]
theorem isBounded_compl_iff : IsBoundedIsBounded sᶜ ↔ IsCobounded s := by
  rw [isBounded_def, isCobounded_def, compl_compl]

Boundedness of Complement iff Coboundedness of Set

Informal description

For any set $s$ in a type $\alpha$ equipped with a bornology, the complement $s^c$ is bounded if and only if $s$ is cobounded.

Bornology.isCobounded_compl_iff theorem

: IsCobounded sᶜ ↔ IsBounded s

Full source

@[simp]
theorem isCobounded_compl_iff : IsCoboundedIsCobounded sᶜ ↔ IsBounded s :=
  Iff.rfl

Complement of a Set is Cobounded iff the Set is Bounded

Informal description

For any set $s$ in a bornology on $\alpha$, the complement $s^c$ is cobounded if and only if $s$ is bounded.

Bornology.isBounded_empty theorem

: IsBounded (∅ : Set α)

Full source

@[simp]
theorem isBounded_empty : IsBounded (∅ : Set α) := by
  rw [isBounded_def, compl_empty]
  exact univ_mem

Boundedness of the Empty Set in a Bornology

Informal description

In any bornology on a type $\alpha$, the empty set $\emptyset$ is bounded.

Bornology.nonempty_of_not_isBounded theorem

(h : ¬IsBounded s) : s.Nonempty

Full source

theorem nonempty_of_not_isBounded (h : ¬IsBounded s) : s.Nonempty := by
  rw [nonempty_iff_ne_empty]
  rintro rfl
  exact h isBounded_empty

Nonemptiness of Unbounded Sets in a Bornology

Informal description

If a set $s$ in a bornology on $\alpha$ is not bounded, then $s$ is nonempty. In other words, $\neg \text{IsBounded}(s) \implies s \neq \emptyset$.

Bornology.isBounded_singleton theorem

: IsBounded ({ x } : Set α)

Full source

@[simp]
theorem isBounded_singleton : IsBounded ({x} : Set α) := by
  rw [isBounded_def]
  exact le_cofinite _ (finite_singleton x).compl_mem_cofinite

Boundedness of Singleton Sets in a Bornology

Informal description

For any element $x$ of a type $\alpha$ equipped with a bornology, the singleton set $\{x\}$ is bounded.

Bornology.isBounded_iff_forall_mem theorem

: IsBounded s ↔ ∀ x ∈ s, IsBounded s

Full source

theorem isBounded_iff_forall_mem : IsBoundedIsBounded s ↔ ∀ x ∈ s, IsBounded s :=
  ⟨fun h _ _ ↦ h, fun h ↦ by
    rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
    exacts [isBounded_empty, h x hx]⟩

Boundedness of a Set is Equivalent to Boundedness at Every Point

Informal description

A set $s$ in a bornology is bounded if and only if every element $x \in s$ implies that $s$ itself is bounded.

Bornology.isCobounded_univ theorem

: IsCobounded (univ : Set α)

Full source

@[simp]
theorem isCobounded_univ : IsCobounded (univ : Set α) :=
  univ_mem

Universal Set is Cobounded in Any Bornology

Informal description

In any bornology on a type $\alpha$, the universal set $\text{univ} : \text{Set } \alpha$ is cobounded, i.e., its complement is bounded.

Bornology.isCobounded_inter theorem

: IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t

Full source

@[simp]
theorem isCobounded_inter : IsCoboundedIsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t :=
  inter_mem_iff

Intersection of Cobounded Sets is Cobounded if and only if Both Sets are Cobounded

Informal description

For any sets $s$ and $t$ in a bornology on a type $\alpha$, the intersection $s \cap t$ is cobounded if and only if both $s$ and $t$ are cobounded.

Bornology.IsCobounded.inter theorem

(hs : IsCobounded s) (ht : IsCobounded t) : IsCobounded (s ∩ t)

Full source

theorem IsCobounded.inter (hs : IsCobounded s) (ht : IsCobounded t) : IsCobounded (s ∩ t) :=
  isCobounded_inter.2 ⟨hs, ht⟩

Intersection of Cobounded Sets is Cobounded

Informal description

For any two cobounded sets $s$ and $t$ in a bornology on a type $\alpha$, their intersection $s \cap t$ is also cobounded.

Bornology.isBounded_union theorem

: IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Full source

@[simp]
theorem isBounded_union : IsBoundedIsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t := by
  simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

Union of Bounded Sets is Bounded if and only if Both Sets are Bounded

Informal description

For any two sets $s$ and $t$ in a bornology on a type $\alpha$, the union $s \cup t$ is bounded if and only if both $s$ and $t$ are bounded.

Bornology.IsBounded.union theorem

(hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ∪ t)

Full source

theorem IsBounded.union (hs : IsBounded s) (ht : IsBounded t) : IsBounded (s ∪ t) :=
  isBounded_union.2 ⟨hs, ht⟩

Union of Bounded Sets is Bounded

Informal description

For any two sets $s$ and $t$ in a type $\alpha$ equipped with a bornology, if $s$ and $t$ are both bounded, then their union $s \cup t$ is also bounded.

Bornology.IsCobounded.superset theorem

(hs : IsCobounded s) (ht : s ⊆ t) : IsCobounded t

Full source

theorem IsCobounded.superset (hs : IsCobounded s) (ht : s ⊆ t) : IsCobounded t :=
  mem_of_superset hs ht

Superset of a Cobounded Set is Cobounded

Informal description

If a set $s$ is cobounded in a bornology and $s$ is a subset of another set $t$, then $t$ is also cobounded.

Bornology.IsBounded.subset theorem

(ht : IsBounded t) (hs : s ⊆ t) : IsBounded s

Full source

theorem IsBounded.subset (ht : IsBounded t) (hs : s ⊆ t) : IsBounded s :=
  ht.superset (compl_subset_compl.mpr hs)

Subset of a Bounded Set is Bounded

Informal description

For any sets $s$ and $t$ in a type $\alpha$ equipped with a bornology, if $t$ is bounded and $s$ is a subset of $t$, then $s$ is also bounded.

Bornology.sUnion_bounded_univ theorem

: ⋃₀ {s : Set α | IsBounded s} = univ

Full source

@[simp]
theorem sUnion_bounded_univ : ⋃₀ { s : Set α | IsBounded s } = univ :=
  sUnion_eq_univ_iff.2 fun a => ⟨{a}, isBounded_singleton, mem_singleton a⟩

Union of Bounded Sets Covers the Universal Set

Informal description

The union of all bounded subsets of a type $\alpha$ equipped with a bornology equals the universal set $\text{univ}$ (the set of all elements of $\alpha$). In other words, every element of $\alpha$ is contained in some bounded set.

Bornology.IsBounded.insert theorem

(h : IsBounded s) (x : α) : IsBounded (insert x s)

Full source

theorem IsBounded.insert (h : IsBounded s) (x : α) : IsBounded (insert x s) :=
  isBounded_singleton.union h

Insertion Preserves Boundedness in a Bornology

Informal description

For any bounded set $s$ in a type $\alpha$ equipped with a bornology, and for any element $x \in \alpha$, the set obtained by inserting $x$ into $s$ (i.e., $\{x\} \cup s$) is also bounded.

Bornology.isBounded_insert theorem

: IsBounded (insert x s) ↔ IsBounded s

Full source

@[simp]
theorem isBounded_insert : IsBoundedIsBounded (insert x s) ↔ IsBounded s :=
  ⟨fun h ↦ h.subset (subset_insert _ _), (.insert · x)⟩

Boundedness of Insertion: $\text{IsBounded}(\{x\} \cup s) \leftrightarrow \text{IsBounded}(s)$

Informal description

For any element $x$ of a type $\alpha$ equipped with a bornology and any subset $s \subseteq \alpha$, the set $\{x\} \cup s$ is bounded if and only if $s$ is bounded.

Bornology.comap_cobounded_le_iff theorem

 [Bornology β] {f : α → β} : (cobounded β).comap f ≤ cobounded α ↔ ∀ ⦃s⦄, IsBounded s → IsBounded (f '' s)

Full source

theorem comap_cobounded_le_iff [Bornology β] {f : α → β} :
    (cobounded β).comap f ≤ cobounded α ↔ ∀ ⦃s⦄, IsBounded s → IsBounded (f '' s) := by
  refine
    ⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
  obtain ⟨t, ht, hts⟩ := h hs.compl
  rw [subset_compl_comm, ← preimage_compl] at hts
  exact (IsCobounded.compl ht).subset ((image_subset f hts).trans <| image_preimage_subset _ _)

Characterization of Bornology-Preserving Maps via Cobounded Filters

Informal description

Let $\alpha$ and $\beta$ be types equipped with bornologies. For a function $f : \alpha \to \beta$, the following are equivalent: 1. The pullback of the cobounded filter on $\beta$ under $f$ is contained in the cobounded filter on $\alpha$. 2. For every bounded set $s \subseteq \alpha$, the image $f(s) \subseteq \beta$ is bounded. In other words, the inequality $\text{cobounded}(\beta) \circ f \leq \text{cobounded}(\alpha)$ holds if and only if $f$ maps bounded sets to bounded sets.

Bornology.ext_iff' theorem

{t t' : Bornology α} : t = t' ↔ ∀ s, s ∈ @cobounded α t ↔ s ∈ @cobounded α t'

Full source

theorem ext_iff' {t t' : Bornology α} :
    t = t' ↔ ∀ s, s ∈ @cobounded α t ↔ s ∈ @cobounded α t' :=
  Bornology.ext_iff.trans Filter.ext_iff

Equality of Bornologies via Cobounded Sets

Informal description

Two bornologies $t$ and $t'$ on a type $\alpha$ are equal if and only if for every set $s \subseteq \alpha$, $s$ is cobounded in $t$ if and only if $s$ is cobounded in $t'$.

Bornology.ext_iff_isBounded theorem

{t t' : Bornology α} : t = t' ↔ ∀ s, @IsBounded α t s ↔ @IsBounded α t' s

Full source

theorem ext_iff_isBounded {t t' : Bornology α} :
    t = t' ↔ ∀ s, @IsBounded α t s ↔ @IsBounded α t' s :=
  ext_iff'.trans compl_surjective.forall

Equality of Bornologies via Bounded Sets

Informal description

Two bornologies $t$ and $t'$ on a type $\alpha$ are equal if and only if for every subset $s \subseteq \alpha$, $s$ is bounded in $t$ if and only if $s$ is bounded in $t'$.

Bornology.isCobounded_ofBounded_iff theorem

 (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
  @IsCobounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ sᶜ ∈ B

Full source

theorem isCobounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
    @IsCobounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ sᶜ ∈ B :=
  Iff.rfl

Characterization of Cobounded Sets in Bornology Constructed from Bounded Sets

Informal description

Given a type $\alpha$ and a collection $B$ of subsets of $\alpha$ satisfying: 1. $\emptyset \in B$, 2. If $s_1 \in B$ and $s_2 \subseteq s_1$, then $s_2 \in B$, 3. If $s_1, s_2 \in B$, then $s_1 \cup s_2 \in B$, 4. For any $x \in \alpha$, $\{x\} \in B$, then for the bornology constructed from $B$ via `Bornology.ofBounded`, a set $s \subseteq \alpha$ is cobounded (i.e., $s^c$ is bounded) if and only if the complement of $s$ belongs to $B$.

Bornology.isBounded_ofBounded_iff theorem

 (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
  @IsBounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ s ∈ B

Full source

theorem isBounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
    @IsBounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ s ∈ B := by
  rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]

Characterization of Bounded Sets in Bornology Constructed from Bounded Sets

Informal description

Given a type $\alpha$ and a collection $B$ of subsets of $\alpha$ satisfying: 1. $\emptyset \in B$, 2. If $s_1 \in B$ and $s_2 \subseteq s_1$, then $s_2 \in B$, 3. If $s_1, s_2 \in B$, then $s_1 \cup s_2 \in B$, 4. For any $x \in \alpha$, $\{x\} \in B$, then for the bornology constructed from $B$ via `Bornology.ofBounded`, a set $s \subseteq \alpha$ is bounded if and only if $s \in B$.

Bornology.isCobounded_biInter theorem

{s : Set ι} {f : ι → Set α} (hs : s.Finite) : IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i)

Full source

theorem isCobounded_biInter {s : Set ι} {f : ι → Set α} (hs : s.Finite) :
    IsCoboundedIsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i) :=
  biInter_mem hs

Finite Intersection of Cobounded Sets is Cobounded if and only if Each Set is Cobounded

Informal description

Let $\alpha$ be a type equipped with a bornology, $\iota$ be an index type, $s \subseteq \iota$ be a finite subset, and $f : \iota \to \text{Set } \alpha$ be a family of sets. Then the intersection $\bigcap_{i \in s} f(i)$ is cobounded (i.e., its complement is bounded) if and only if for every $i \in s$, the set $f(i)$ is cobounded.

Bornology.isCobounded_biInter_finset theorem

(s : Finset ι) {f : ι → Set α} : IsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i)

Full source

@[simp]
theorem isCobounded_biInter_finset (s : Finset ι) {f : ι → Set α} :
    IsCoboundedIsCobounded (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i) :=
  biInter_finset_mem s

Finite Intersection of Cobounded Sets is Cobounded iff Each Set is Cobounded

Informal description

Let $\alpha$ be a type equipped with a bornology, $\iota$ be an index type, $s$ be a finite set of indices of type $\iota$, and $f : \iota \to \text{Set } \alpha$ be a family of sets. Then the intersection $\bigcap_{i \in s} f(i)$ is cobounded (i.e., its complement is bounded) if and only if for every $i \in s$, the set $f(i)$ is cobounded.

Bornology.isCobounded_iInter theorem

[Finite ι] {f : ι → Set α} : IsCobounded (⋂ i, f i) ↔ ∀ i, IsCobounded (f i)

Full source

@[simp]
theorem isCobounded_iInter [Finite ι] {f : ι → Set α} :
    IsCoboundedIsCobounded (⋂ i, f i) ↔ ∀ i, IsCobounded (f i) :=
  iInter_mem

Finite Intersection of Cobounded Sets is Cobounded iff Each Set is Cobounded

Informal description

Let $\alpha$ be a type equipped with a bornology, $\iota$ be a finite index type, and $f : \iota \to \text{Set } \alpha$ be a family of sets. Then the intersection $\bigcap_{i \in \iota} f(i)$ is cobounded (i.e., its complement is bounded) if and only if for every $i \in \iota$, the set $f(i)$ is cobounded.

Bornology.isCobounded_sInter theorem

{S : Set (Set α)} (hs : S.Finite) : IsCobounded (⋂₀ S) ↔ ∀ s ∈ S, IsCobounded s

Full source

theorem isCobounded_sInter {S : Set (Set α)} (hs : S.Finite) :
    IsCoboundedIsCobounded (⋂₀ S) ↔ ∀ s ∈ S, IsCobounded s :=
  sInter_mem hs

Finite Intersection of Cobounded Sets is Cobounded iff All Sets are Cobounded

Informal description

Let $\alpha$ be a type equipped with a bornology, and let $S$ be a finite collection of subsets of $\alpha$. Then the intersection $\bigcap S$ is cobounded (i.e., its complement is bounded) if and only if every set $s \in S$ is cobounded.

Bornology.isBounded_biUnion theorem

{s : Set ι} {f : ι → Set α} (hs : s.Finite) : IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Full source

theorem isBounded_biUnion {s : Set ι} {f : ι → Set α} (hs : s.Finite) :
    IsBoundedIsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i) := by
  simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

Finite Union of Bounded Sets is Bounded if and only if Each Set is Bounded

Informal description

Let $\alpha$ be a type equipped with a bornology, $\iota$ be an index type, $s \subseteq \iota$ be a finite subset, and $f : \iota \to \text{Set } \alpha$ be a family of sets. Then the union $\bigcup_{i \in s} f(i)$ is bounded if and only if for every $i \in s$, the set $f(i)$ is bounded.

Bornology.isBounded_biUnion_finset theorem

(s : Finset ι) {f : ι → Set α} : IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Full source

theorem isBounded_biUnion_finset (s : Finset ι) {f : ι → Set α} :
    IsBoundedIsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i) :=
  isBounded_biUnion s.finite_toSet

Boundedness of Finite Union in Bornology

Informal description

Let $\alpha$ be a type equipped with a bornology, $\iota$ be an index type, $s$ be a finite set of indices (represented as a finset), and $f : \iota \to \text{Set } \alpha$ be a family of sets. Then the union $\bigcup_{i \in s} f(i)$ is bounded if and only if for every $i \in s$, the set $f(i)$ is bounded.

Bornology.isBounded_sUnion theorem

{S : Set (Set α)} (hs : S.Finite) : IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s

Full source

theorem isBounded_sUnion {S : Set (Set α)} (hs : S.Finite) :
    IsBoundedIsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s := by rw [sUnion_eq_biUnion, isBounded_biUnion hs]

Finite Union of Bounded Sets is Bounded if and only if All Sets are Bounded

Informal description

Let $\alpha$ be a type equipped with a bornology, and let $S$ be a finite collection of subsets of $\alpha$. The union $\bigcup_{s \in S} s$ is bounded if and only if every set $s \in S$ is bounded.

Bornology.isBounded_iUnion theorem

[Finite ι] {s : ι → Set α} : IsBounded (⋃ i, s i) ↔ ∀ i, IsBounded (s i)

Full source

@[simp]
theorem isBounded_iUnion [Finite ι] {s : ι → Set α} :
    IsBoundedIsBounded (⋃ i, s i) ↔ ∀ i, IsBounded (s i) := by
  rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

Finite Union is Bounded if and only if All Sets are Bounded

Informal description

Let $\alpha$ be a type equipped with a bornology, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by a finite type $\iota$. The union $\bigcup_{i \in \iota} s_i$ is bounded if and only if each set $s_i$ is bounded.

Bornology.eventually_ne_cobounded theorem

(a : α) : ∀ᶠ x in cobounded α, x ≠ a

Full source

lemma eventually_ne_cobounded (a : α) : ∀ᶠ x in cobounded α, x ≠ a :=
  le_cofinite_iff_eventually_ne.1 (le_cofinite _) a

Eventual Non-Equality in Cobounded Filter

Informal description

For any element $a$ in a type $\alpha$ equipped with a bornology, the event that $x \neq a$ holds eventually in the filter of cobounded sets. In other words, the set $\{x \in \alpha \mid x \neq a\}$ is cobounded.

Filter.HasBasis.disjoint_cobounded_iff theorem

 [Bornology α] {ι : Sort*} {p : ι → Prop} {s : ι → Set α} {l : Filter α} (h : l.HasBasis p s) :
  Disjoint l (cobounded α) ↔ ∃ i, p i ∧ Bornology.IsBounded (s i)

Full source

theorem Filter.HasBasis.disjoint_cobounded_iff [Bornology α] {ι : Sort*} {p : ι → Prop}
    {s : ι → Set α} {l : Filter α} (h : l.HasBasis p s) :
    DisjointDisjoint l (cobounded α) ↔ ∃ i, p i ∧ Bornology.IsBounded (s i) :=
  h.disjoint_iff_left

Disjointness of a Filter and the Cobounded Filter via Basis Elements

Informal description

Let $\alpha$ be a type equipped with a bornology, and let $l$ be a filter on $\alpha$ with a basis $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then $l$ is disjoint from the cobounded filter if and only if there exists an index $i \in \iota$ such that $p(i)$ holds and the set $s_i$ is bounded in the bornology.

Set.Finite.isBounded theorem

[Bornology α] {s : Set α} (hs : s.Finite) : IsBounded s

Full source

theorem Set.Finite.isBounded [Bornology α] {s : Set α} (hs : s.Finite) : IsBounded s :=
  Bornology.le_cofinite α hs.compl_mem_cofinite

Finite sets are bounded in any bornology

Informal description

For any bornology on a type $\alpha$, every finite subset $s \subseteq \alpha$ is bounded.

Filter.Tendsto.eventually_ne_cobounded theorem

[Bornology α] {f : β → α} {l : Filter β} (h : Tendsto f l (cobounded α)) (a : α) : ∀ᶠ x in l, f x ≠ a

Full source

nonrec lemma Filter.Tendsto.eventually_ne_cobounded [Bornology α] {f : β → α} {l : Filter β}
    (h : Tendsto f l (cobounded α)) (a : α) : ∀ᶠ x in l, f x ≠ a :=
  h.eventually <| eventually_ne_cobounded a

Eventual Non-Equality under Tendency to Cobounded Filter

Informal description

Let $\alpha$ be a type equipped with a bornology, and let $f : \beta \to \alpha$ be a function. If $f$ tends to the cobounded filter along a filter $l$ on $\beta$, then for any $a \in \alpha$, the event that $f(x) \neq a$ holds eventually in $l$.

instBornologyPUnit instance

: Bornology PUnit

Full source

instance : Bornology PUnit :=
  ⟨⊥, bot_le⟩

Bornology Structure on PUnit

Informal description

The punit type (a type with exactly one element) has a canonical bornology structure where every set is bounded.

Bornology.cofinite abbrev

: Bornology α

Full source

/-- The cofinite filter as a bornology -/
abbrev Bornology.cofinite : Bornology α where
  cobounded' := Filter.cofinite
  le_cofinite' := le_rfl

Cofinite Bornology Structure

Informal description

The cofinite filter on a type $\alpha$ defines a bornology structure where a set is cobounded if and only if its complement is finite. In other words, the bornology structure is given by the filter of subsets of $\alpha$ with finite complement.

BoundedSpace structure

(α : Type*) [Bornology α]

Full source

/-- A space with a `Bornology` is a **bounded space** if `Set.univ : Set α` is bounded. -/
class BoundedSpace (α : Type*) [Bornology α] : Prop where
  /-- The `Set.univ` is bounded. -/
  bounded_univ : Bornology.IsBounded (univ : Set α)

Bounded Space

Informal description

A `BoundedSpace` is a space equipped with a bornology where the entire space is bounded, i.e., the complement of the universal set is cobounded. This means that in a bounded space, the filter of cobounded sets contains the empty set's complement (which is the universal set itself).

BoundedSpace.of_finite instance

{α : Type*} [Bornology α] [Finite α] : BoundedSpace α

Full source

/-- A finite space is bounded. -/
instance (priority := 100) BoundedSpace.of_finite {α : Type*} [Bornology α] [Finite α] :
    BoundedSpace α where
  bounded_univ := (toFinite _).isBounded

Finite Spaces are Bounded

Informal description

For any type $\alpha$ equipped with a bornology, if $\alpha$ is finite, then the entire space $\alpha$ is bounded.

Bornology.isBounded_univ theorem

: IsBounded (univ : Set α) ↔ BoundedSpace α

Full source

theorem isBounded_univ : IsBoundedIsBounded (univ : Set α) ↔ BoundedSpace α :=
  ⟨fun h => ⟨h⟩, fun h => h.1⟩

Universal Set Boundedness Criterion for Bounded Spaces

Informal description

For a type $\alpha$ equipped with a bornology, the universal set $\text{univ} \subseteq \alpha$ is bounded if and only if $\alpha$ is a bounded space.

Bornology.cobounded_eq_bot_iff theorem

: cobounded α = ⊥ ↔ BoundedSpace α

Full source

theorem cobounded_eq_bot_iff : coboundedcobounded α = ⊥ ↔ BoundedSpace α := by
  rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]

Cobounded Filter Triviality Criterion for Bounded Spaces

Informal description

The cobounded filter on a type $\alpha$ equipped with a bornology is equal to the bottom filter (i.e., contains only the universal set) if and only if $\alpha$ is a bounded space.

Bornology.IsBounded.all theorem

(s : Set α) : IsBounded s

Full source

theorem IsBounded.all (s : Set α) : IsBounded s :=
  BoundedSpace.bounded_univ.subset s.subset_univ

All Sets are Bounded in a Bounded Space

Informal description

In a bounded space $\alpha$, every subset $s \subseteq \alpha$ is bounded.

Bornology.IsCobounded.all theorem

(s : Set α) : IsCobounded s

Full source

theorem IsCobounded.all (s : Set α) : IsCobounded s :=
  compl_compl s ▸ IsBounded.all sᶜ

All Sets are Cobounded in a Bounded Space

Informal description

In a bounded space $\alpha$, every subset $s \subseteq \alpha$ is cobounded, i.e., its complement is bounded.

Bornology.cobounded_eq_bot theorem

: cobounded α = ⊥

Full source

@[simp]
theorem cobounded_eq_bot : cobounded α = ⊥ :=
  cobounded_eq_bot_iff.2 ‹_›

Cobounded Filter Triviality in Bounded Spaces

Informal description

The cobounded filter on a type $\alpha$ equipped with a bornology is equal to the bottom filter (i.e., contains only the universal set).

OrderDual.instBornology instance

: Bornology αᵒᵈ

Full source

instance instBornology : Bornology αᵒᵈ := ‹Bornology α›

Bornology on Order Duals

Informal description

The order dual $\alpha^\mathrm{op}$ of a type $\alpha$ with a bornology inherits a bornology structure where the cobounded sets are preserved under the order-reversing isomorphism.

OrderDual.isCobounded_preimage_ofDual theorem

{s : Set α} : IsCobounded (ofDual ⁻¹' s) ↔ IsCobounded s

Full source

@[simp] lemma isCobounded_preimage_ofDual {s : Set α} :
    IsCoboundedIsCobounded (ofDual ⁻¹' s) ↔ IsCobounded s := Iff.rfl

Coboundedness Preservation under Order Dual Preimage

Informal description

For any set $s \subseteq \alpha$, the preimage of $s$ under the order-reversing isomorphism $\text{ofDual} : \alpha^\text{op} \to \alpha$ is cobounded in the bornology on $\alpha^\text{op}$ if and only if $s$ is cobounded in the bornology on $\alpha$.

OrderDual.isCobounded_preimage_toDual theorem

{s : Set αᵒᵈ} : IsCobounded (toDual ⁻¹' s) ↔ IsCobounded s

Full source

@[simp] lemma isCobounded_preimage_toDual {s : Set αᵒᵈ} :
    IsCoboundedIsCobounded (toDual ⁻¹' s) ↔ IsCobounded s := Iff.rfl

Coboundedness Preservation under Order Dual Preimage

Informal description

For any set $s$ in the order dual $\alpha^\mathrm{op}$ of a type $\alpha$ with a bornology, the preimage of $s$ under the order-reversing map $\mathrm{toDual} : \alpha \to \alpha^\mathrm{op}$ is cobounded in $\alpha$ if and only if $s$ is cobounded in $\alpha^\mathrm{op}$.

OrderDual.isBounded_preimage_ofDual theorem

{s : Set α} : IsBounded (ofDual ⁻¹' s) ↔ IsBounded s

Full source

@[simp] lemma isBounded_preimage_ofDual {s : Set α} :
    IsBoundedIsBounded (ofDual ⁻¹' s) ↔ IsBounded s := Iff.rfl

Boundedness Preservation under Order Dual Preimage

Informal description

For any set $s \subseteq \alpha$, the preimage of $s$ under the order-reversing isomorphism $\alpha^{\text{op}} \to \alpha$ is bounded in the bornology on $\alpha^{\text{op}}$ if and only if $s$ is bounded in the bornology on $\alpha$.

OrderDual.isBounded_preimage_toDual theorem

{s : Set αᵒᵈ} : IsBounded (toDual ⁻¹' s) ↔ IsBounded s

Full source

@[simp] lemma isBounded_preimage_toDual {s : Set αᵒᵈ} :
    IsBoundedIsBounded (toDual ⁻¹' s) ↔ IsBounded s := Iff.rfl

Boundedness Preservation under Order Dual Preimage

Informal description

For any set $s$ in the order dual $\alpha^\mathrm{op}$ of a type $\alpha$ with a bornology, the preimage of $s$ under the canonical map $\alpha \to \alpha^\mathrm{op}$ is bounded in $\alpha$ if and only if $s$ is bounded in $\alpha^\mathrm{op}$.

Main definitions