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 #

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_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.ofBounded and Bornology.ext_iff_isBounded

  • cobounded' : Filter α

    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.

  • le_cofinite' : Bornology.cobounded' Filter.cofinite

    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.

Instances
    theorem Bornology.le_cofinite' {α : Type u_4} [self : Bornology α] :
    Bornology.cobounded' Filter.cofinite

    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.

    def Bornology.cobounded (α : Type u_4) [Bornology α] :

    The filter of cobounded sets in a bornology.

    Equations
    Instances For

      Alias of Bornology.cobounded.


      The filter of cobounded sets in a bornology.

      Equations
      Instances For
        theorem Bornology.le_cofinite (α : Type u_4) [Bornology α] :
        Bornology.cobounded α Filter.cofinite
        theorem Bornology.ext {α : Type u_2} (t : Bornology α) (t' : Bornology α) (h_cobounded : Bornology.cobounded α = Bornology.cobounded α) :
        t = t'
        @[simp]
        theorem Bornology.ofBounded_cobounded {α : Type u_4} (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.cobounded α = Filter.comk (fun (x : Set α) => x B) empty_mem subset_mem union_mem
        def Bornology.ofBounded {α : Type u_4} (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) :

        A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.

        Equations
        Instances For
          @[simp]
          theorem Bornology.ofBounded'_cobounded {α : Type u_4} (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 = Set.univ) :
          Bornology.cobounded α = Filter.comk (fun (x : Set α) => x B) empty_mem subset_mem union_mem
          def Bornology.ofBounded' {α : Type u_4} (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 = Set.univ) :

          A constructor for bornologies by specifying the bounded sets, and showing that they satisfy the appropriate conditions.

          Equations
          Instances For
            def Bornology.IsCobounded {α : Type u_2} [Bornology α] (s : Set α) :

            IsCobounded is the predicate that s is in the filter of cobounded sets in the ambient bornology on α

            Equations
            Instances For
              def Bornology.IsBounded {α : Type u_2} [Bornology α] (s : Set α) :

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

              Equations
              Instances For

                Alias of the reverse direction of Bornology.isBounded_compl_iff.

                Alias of the forward direction of Bornology.isBounded_compl_iff.

                theorem Bornology.IsBounded.compl {α : Type u_2} :

                Alias of the reverse direction of Bornology.isCobounded_compl_iff.

                Alias of the forward direction of Bornology.isCobounded_compl_iff.

                @[simp]
                theorem Bornology.nonempty_of_not_isBounded {α : Type u_2} :
                ∀ {x : Bornology α} {s : Set α}, ¬Bornology.IsBounded ss.Nonempty
                @[simp]
                theorem Bornology.isBounded_singleton {α : Type u_2} :
                ∀ {x : Bornology α} {x_1 : α}, Bornology.IsBounded {x_1}
                theorem Bornology.isBounded_iff_forall_mem {α : Type u_2} :
                ∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded s x_1s, Bornology.IsBounded s
                @[simp]
                theorem Bornology.isCobounded_univ {α : Type u_2} :
                ∀ {x : Bornology α}, Bornology.IsCobounded Set.univ
                theorem Bornology.IsCobounded.superset {α : Type u_2} :
                ∀ {x : Bornology α} {s t : Set α}, Bornology.IsCobounded ss tBornology.IsCobounded t
                theorem Bornology.IsBounded.subset {α : Type u_2} :
                ∀ {x : Bornology α} {s t : Set α}, Bornology.IsBounded ts tBornology.IsBounded s
                @[simp]
                theorem Bornology.sUnion_bounded_univ {α : Type u_2} :
                ∀ {x : Bornology α}, ⋃₀ {s : Set α | Bornology.IsBounded s} = Set.univ
                theorem Bornology.IsBounded.insert {α : Type u_2} :
                ∀ {x : Bornology α} {s : Set α}, Bornology.IsBounded s∀ (x_1 : α), Bornology.IsBounded (insert x_1 s)
                @[simp]
                theorem Bornology.isBounded_insert {α : Type u_2} :
                ∀ {x : Bornology α} {s : Set α} {x_1 : α}, Bornology.IsBounded (insert x_1 s) Bornology.IsBounded s
                theorem Bornology.comap_cobounded_le_iff {α : Type u_2} {β : Type u_3} :
                ∀ {x : Bornology α} [inst : Bornology β] {f : αβ}, Filter.comap f (Bornology.cobounded β) Bornology.cobounded α ∀ ⦃s : Set α⦄, Bornology.IsBounded sBornology.IsBounded (f '' s)
                theorem Bornology.ext_iff' {α : Type u_2} {t : Bornology α} {t' : Bornology α} :
                t = t' ∀ (s : Set α), s Bornology.cobounded α s Bornology.cobounded α
                theorem Bornology.ext_iff_isBounded {α : Type u_2} {t : Bornology α} {t' : Bornology α} :
                theorem Bornology.isCobounded_ofBounded_iff {α : Type u_2} {s : Set α} (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 : ∀ (x : α), {x} B} :
                theorem Bornology.isBounded_ofBounded_iff {α : Type u_2} {s : Set α} (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 : ∀ (x : α), {x} B} :
                theorem Bornology.isCobounded_biInter {ι : Type u_1} {α : Type u_2} [Bornology α] {s : Set ι} {f : ιSet α} (hs : s.Finite) :
                Bornology.IsCobounded (is, f i) is, Bornology.IsCobounded (f i)
                @[simp]
                theorem Bornology.isCobounded_biInter_finset {ι : Type u_1} {α : Type u_2} [Bornology α] (s : Finset ι) {f : ιSet α} :
                Bornology.IsCobounded (is, f i) is, Bornology.IsCobounded (f i)
                @[simp]
                theorem Bornology.isCobounded_iInter {ι : Type u_1} {α : Type u_2} [Bornology α] [Finite ι] {f : ιSet α} :
                Bornology.IsCobounded (⋂ (i : ι), f i) ∀ (i : ι), Bornology.IsCobounded (f i)
                theorem Bornology.isCobounded_sInter {α : Type u_2} [Bornology α] {S : Set (Set α)} (hs : S.Finite) :
                theorem Bornology.isBounded_biUnion {ι : Type u_1} {α : Type u_2} [Bornology α] {s : Set ι} {f : ιSet α} (hs : s.Finite) :
                Bornology.IsBounded (is, f i) is, Bornology.IsBounded (f i)
                theorem Bornology.isBounded_biUnion_finset {ι : Type u_1} {α : Type u_2} [Bornology α] (s : Finset ι) {f : ιSet α} :
                Bornology.IsBounded (is, f i) is, Bornology.IsBounded (f i)
                theorem Bornology.isBounded_sUnion {α : Type u_2} [Bornology α] {S : Set (Set α)} (hs : S.Finite) :
                @[simp]
                theorem Bornology.isBounded_iUnion {ι : Type u_1} {α : Type u_2} [Bornology α] [Finite ι] {s : ιSet α} :
                Bornology.IsBounded (⋃ (i : ι), s i) ∀ (i : ι), Bornology.IsBounded (s i)
                theorem Bornology.eventually_ne_cobounded {α : Type u_2} [Bornology α] (a : α) :
                ∀ᶠ (x : α) in Bornology.cobounded α, x a
                theorem Filter.HasBasis.disjoint_cobounded_iff {α : Type u_2} [Bornology α] {ι : Sort u_4} {p : ιProp} {s : ιSet α} {l : Filter α} (h : l.HasBasis p s) :
                Disjoint l (Bornology.cobounded α) ∃ (i : ι), p i Bornology.IsBounded (s i)
                theorem Set.Finite.isBounded {α : Type u_2} [Bornology α] {s : Set α} (hs : s.Finite) :
                theorem Filter.Tendsto.eventually_ne_cobounded {α : Type u_2} {β : Type u_3} [Bornology α] {f : βα} {l : Filter β} (h : Filter.Tendsto f l (Bornology.cobounded α)) (a : α) :
                ∀ᶠ (x : β) in l, f x a
                @[reducible, inline]
                abbrev Bornology.cofinite {α : Type u_2} :

                The cofinite filter as a bornology

                Equations
                • Bornology.cofinite = { cobounded' := Filter.cofinite, le_cofinite' := }
                Instances For
                  class BoundedSpace (α : Type u_4) [Bornology α] :

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

                  Instances
                    theorem BoundedSpace.bounded_univ {α : Type u_4} [Bornology α] [self : BoundedSpace α] :

                    The Set.univ is bounded.

                    @[instance 100]
                    instance BoundedSpace.of_finite {α : Type u_4} [Bornology α] [Finite α] :

                    A finite space is bounded.

                    Equations
                    • =
                    Equations
                    • OrderDual.instBornology = inst
                    @[simp]
                    @[simp]
                    theorem OrderDual.isBounded_preimage_ofDual {α : Type u_2} [Bornology α] {s : Set α} :
                    @[simp]