Bornology.le_cofinite
theorem Bornology.le_cofinite : ∀ (α : Type u_4) [inst : Bornology α], Bornology.cobounded α ≤ Filter.cofinite := by
sorry
The theorem `Bornology.le_cofinite` asserts that for any type `α` equipped with a Bornology structure, the filter of cobounded sets in that Bornology is a sub-filter of the cofinite filter. In other words, every cobounded set in the Bornology is also a set whose complement is finite. Thus the filter of all cobounded sets includes all sets whose complement is finite.
More concisely: The filter of cobounded sets in a Bornology is a sub-filter of the cofinite filter.
|
Bornology.cobounded_eq_bot
theorem Bornology.cobounded_eq_bot :
∀ (α : Type u_2) [inst : Bornology α] [inst_1 : BoundedSpace α], Bornology.cobounded α = ⊥
This theorem states that for any type `α` equipped with a Bornology structure and assumed to be a Bounded Space, the filter of cobounded sets in this Bornology is the bottom filter. In other words, in a bounded space, there are no cobounded sets in the corresponding Bornology, or the concept of cobounded sets becomes trivial.
More concisely: In a bounded space equipped with a Bornology structure, the filter of cobounded sets is the bottom filter.
|
Bornology.IsBounded.union
theorem Bornology.IsBounded.union :
∀ {α : Type u_2} {x : Bornology α} {s t : Set α},
Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s ∪ t)
The theorem `Bornology.IsBounded.union` states that for any type 'α' with a bornology 'x' and any two sets 's' and 't' of type 'α', if 's' and 't' are both bounded relative to the bornology 'x', then the union of 's' and 't' is also bounded relative to the same bornology. In other words, the union of two bounded sets in a bornological space is again a bounded set.
More concisely: If 'α' is a type with bornology 'x', and 's' and 't' are bounded subsets of 'α' relative to 'x', then their union is also a bounded subset of 'α' relative to 'x'.
|
Bornology.IsBounded.of_compl
theorem Bornology.IsBounded.of_compl :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded sᶜ → Bornology.IsCobounded s
The theorem `Bornology.IsBounded.of_compl` states that for any type `α` with a given bornology `x` and any set `s` of elements of type `α`, if the complement of `s` (denoted by `sᶜ`) is bounded in the bornology, then `s` is cobounded in the bornology.
In other words, if a set's complement is bounded within a particular bornological structure, then the set itself is cobounded, meaning its extent is limited by the structure of the bornology. This theorem is an alias of the forward direction of `Bornology.isBounded_compl_iff`.
More concisely: If the complement of a set in a bornology is bounded, then the set is cobounded.
|
Bornology.le_cofinite'
theorem Bornology.le_cofinite' : ∀ {α : Type u_4} [self : Bornology α], Bornology.cobounded' ≤ Filter.cofinite := by
sorry
The theorem `Bornology.le_cofinite'` states that for any type `α` with a given Bornology structure, the cobounded filter of the Bornology is a subfilter of the cofinite filter. Here, cobounded filter refers to the filter of sets that are not bounded away from all other points in the structure, while cofinite filter refers to the filter of subsets of `α` whose complements are finite. The theorem essentially compares the size or containment of these two filters, with the cobounded filter being "smaller" or contained within the cofinite filter. This theorem is a property of the Bornology structure, and it's recommended to use `Bornology.le_cofinite` for clarity, as it explicitly includes the `α` argument.
More concisely: The cobounded filter of a Bornology structure is contained in the cofinite filter.
|
Bornology.IsCobounded.of_compl
theorem Bornology.IsCobounded.of_compl :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded sᶜ → Bornology.IsBounded s
This theorem, named as "Bornology.IsCobounded.of_compl", states that for any type `α` endowed with a bornology `x` and any set `s` of type `α`, if the complement of the set `s` (denoted by `sᶜ`) is cobounded in the ambient bornology, then the set `s` itself is bounded relative to the same bornology. In other words, it provides a way to conclude that a set is bounded given the coboundedness of its complement within the context of a certain bornology.
More concisely: If a set's complement is cobounded in a bornology, then the set is bounded in that bornology.
|
Mathlib.Topology.Bornology.Basic._auxLemma.4
theorem Mathlib.Topology.Bornology.Basic._auxLemma.4 :
∀ {α : Type u_2} {x : Bornology α}, Bornology.IsBounded ∅ = True
This theorem is stating that for any type `α` and any bornology `x` on `α`, the set of empty elements, denoted by `∅`, is always bounded relative to the ambient bornology on `α`. In other words, it says that an empty set is always bounded in any given bornology.
More concisely: For any type `α` and bornology `x` on `α`, the empty set `∅` is a bounded subset of `α` relative to `x`.
|
Bornology.IsBounded.subset
theorem Bornology.IsBounded.subset :
∀ {α : Type u_2} {x : Bornology α} {s t : Set α}, Bornology.IsBounded t → s ⊆ t → Bornology.IsBounded s
The theorem `Bornology.IsBounded.subset` states that for any type `α` and any bornology `x` on `α`, if `t` is a bounded set within this bornology, and `s` is a subset of `t`, then `s` is also bounded within the bornology. In other words, the property of being bounded is preserved under taking subsets.
More concisely: If `α` is a type, `x` is a bornology on `α`, `t` is a bounded set in `x`, and `s` is a subset of `t`, then `s` is a bounded set in `x`.
|
Bornology.IsCobounded.compl
theorem Bornology.IsCobounded.compl :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded s → Bornology.IsBounded sᶜ
This theorem states that, for any type `α` and any bornology `x` on `α`, given a set `s` of type `α`, if `s` is cobounded in the given bornology, then the complement of `s` is bounded in the same bornology. In other words, the concept of being cobounded for a set in a specific bornology implies that its complement will be bounded in that bornology.
More concisely: If a set `s` of type `α` is cobounded in the bornology `x` on `α`, then the complement of `s` is bounded in `x`.
|
Bornology.eventually_ne_cobounded
theorem Bornology.eventually_ne_cobounded :
∀ {α : Type u_2} [inst : Bornology α] (a : α), ∀ᶠ (x : α) in Bornology.cobounded α, x ≠ a
The theorem `Bornology.eventually_ne_cobounded` states that for any type `α` equipped with a Bornology (a set of subsets known as "bounded sets"), and for any element `a` of this type, there is a filter (a generalization of a sequence) of elements of `α` that are not equal to `a`, and these elements are obtained from the cobounded sets of the Bornology (i.e., those sets in the Bornology that are not contained in any other set of the Bornology). This essentially says that given any point in a space with a Bornology, we can find a sequence of different points that are all part of large (in a sense defined by the Bornology) sets.
More concisely: For any type `α` with a Bornology and any `a` in `α`, there exists a filter of cobounded sets containing elements not equal to `a`.
|
Bornology.isCobounded_def
theorem Bornology.isCobounded_def :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded s ↔ s ∈ Bornology.cobounded α
The theorem `Bornology.isCobounded_def` states that for any type `α` endowed with a bornology `x` and any set `s` of type `α`, `s` is cobounded in the bornology if and only if `s` belongs to the filter of cobounded sets in the bornology on `α`. In other words, a set is cobounded in a bornology if it is included in the collection of all sets that are cobounded in that bornology.
More concisely: A set is cobounded in a bornology if and only if it belongs to the filter of cobounded sets in that bornology.
|
Bornology.isBounded_univ
theorem Bornology.isBounded_univ :
∀ {α : Type u_2} [inst : Bornology α], Bornology.IsBounded Set.univ ↔ BoundedSpace α
This theorem states that for any type `α` with a specified bornology (a collection of bounded sets), the universal set `Set.univ` (which contains all elements of `α`) is considered to be a bounded set if and only if `α` itself is a bounded space. In other words, it establishes an equivalence between the property of the entire space `α` being bounded and the universal set of `α` being bounded in the context of the given bornology.
More concisely: The universal set of a type `α` is bounded in its bornology if and only if `α` is a bounded space.
|
Bornology.IsBounded.compl
theorem Bornology.IsBounded.compl :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s → Bornology.IsCobounded sᶜ
The theorem `Bornology.IsBounded.compl` states that for any type `α` and any bornology `x` on `α`, if a set `s` of type `α` is bounded with respect to the bornology `x`, then the complement of the set `s` is cobounded with respect to the same bornology. In other words, the boundedness of a set implies the coboundedness of its complement in the context of a given bornology.
More concisely: If a set is bounded in a bornology, then its complement is cobounded in the same bornology.
|
Set.Finite.isBounded
theorem Set.Finite.isBounded : ∀ {α : Type u_2} [inst : Bornology α] {s : Set α}, s.Finite → Bornology.IsBounded s := by
sorry
This theorem states that for any type `α` that has a bornology structure, and for any set `s` of elements of that type, if the set `s` is finite, then it is also bounded with respect to the bornology on `α`. In other words, finite sets are always bounded in any bornology.
More concisely: For any type `α` with a bornology structure and any finite set `s` of elements from `α`, `s` is bounded in the bornology on `α`.
|
BoundedSpace.bounded_univ
theorem BoundedSpace.bounded_univ :
∀ {α : Type u_4} [inst : Bornology α] [self : BoundedSpace α], Bornology.IsBounded Set.univ
This theorem states that the universal set is always bounded. Specifically, for any type `α` that has a Bornology structure (which provides a notion of 'boundedness') and is also a BoundedSpace (meaning that all subsets of `α` are bounded), the universal set, which includes all elements of the type `α`, is bounded according to the definition of the Bornology.
More concisely: If `α` is a type equipped with a Bornology structure and is a BoundedSpace, then the universal set of `α` is bounded in the sense of its Bornology structure.
|
Bornology.isBounded_biUnion
theorem Bornology.isBounded_biUnion :
∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] {s : Set ι} {f : ι → Set α},
s.Finite → (Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i))
This theorem states that for any type `α` with a given bornology and any finite set `s` of elements of type `ι`, the union of the sets `f i` (where `i` ranges over `s`) is bounded in the bornology iff each individual set `f i` is bounded in the bornology. In other words, a finite union of sets is bounded if and only if each of the constituent sets is bounded, given the bornology structure on the underlying type.
More concisely: For any bornology on a type `α` and finite set `s` of `ι`, the union of the bounded sets `f i` (where `i` ranges over `s`) is bounded if and only if each `f i` is bounded.
|
Bornology.isBounded_def
theorem Bornology.isBounded_def :
∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s ↔ sᶜ ∈ Bornology.cobounded α
The theorem `Bornology.isBounded_def` states that for any type `α` with a bornology `x`, and for any set `s` of type `α`, the set `s` is bounded with respect to the bornology if and only if the complement of `s` belongs to the filter of cobounded sets in the bornology of `α`. In other words, the notion of a set being 'bounded' in a bornology is equivalent to its complement being 'cobounded' within the same bornology.
More concisely: A set in a bornology is bounded if and only if its complement is cobounded.
|