Documentation

Mathlib.Data.Analysis.Topology

Computational realization of topological spaces (experimental) #

This file provides infrastructure to compute with topological spaces.

Main declarations #

structure Ctop (α : Type u_1) (σ : Type u_2) :
Type (max u_1 u_2)

A Ctop α σ is a realization of a topology (basis) on α, represented by a type σ together with operations for the top element and the intersection operation.

  • f : σSet α
  • top : ασ
  • top_mem : ∀ (x : α), x self.f (self.top x)
  • inter : (a b : σ) → (x : α) → x self.f a self.f bσ
  • inter_mem : ∀ (a b : σ) (x : α) (h : x self.f a self.f b), x self.f (self.inter a b x h)
  • inter_sub : ∀ (a b : σ) (x : α) (h : x self.f a self.f b), self.f (self.inter a b x h) self.f a self.f b
Instances For
    theorem Ctop.top_mem {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (x : α) :
    x self.f (self.top x)
    theorem Ctop.inter_mem {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a : σ) (b : σ) (x : α) (h : x self.f a self.f b) :
    x self.f (self.inter a b x h)
    theorem Ctop.inter_sub {α : Type u_1} {σ : Type u_2} (self : Ctop α σ) (a : σ) (b : σ) (x : α) (h : x self.f a self.f b) :
    self.f (self.inter a b x h) self.f a self.f b
    instance instInhabitedCtopSet {α : Type u_1} :
    Inhabited (Ctop α (Set α))
    Equations
    • One or more equations did not get rendered due to their size.
    instance Ctop.instCoeFunForallSet {α : Type u_1} {σ : Type u_3} :
    CoeFun (Ctop α σ) fun (x : Ctop α σ) => σSet α
    Equations
    • Ctop.instCoeFunForallSet = { coe := Ctop.f }
    theorem Ctop.coe_mk {α : Type u_1} {σ : Type u_3} (f : σSet α) (T : ασ) (h₁ : ∀ (x : α), x f (T x)) (I : (a b : σ) → (x : α) → x f a f bσ) (h₂ : ∀ (a b : σ) (x : α) (h : x f a f b), x f (I a b x h)) (h₃ : ∀ (a b : σ) (x : α) (h : x f a f b), f (I a b x h) f a f b) (a : σ) :
    { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ }.f a = f a
    def Ctop.ofEquiv {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) :
    Ctop α σCtop α τ

    Map a Ctop to an equivalent representation type.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Ctop.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : Ctop α σ) (a : τ) :
      (Ctop.ofEquiv E F).f a = F.f (E.symm a)
      def Ctop.toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

      Every Ctop is a topological space.

      Equations
      Instances For
        @[simp]
        theorem Ctop.mem_nhds_toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) {s : Set α} {a : α} :
        s nhds a ∃ (b : σ), a F.f b F.f b s
        structure Ctop.Realizer (α : Type u_6) [T : TopologicalSpace α] :
        Type (max (u_5 + 1) u_6)

        A Ctop realizer for the topological space T is a Ctop which generates T.

        • σ : Type u_5
        • F : Ctop α self
        • eq : self.F.toTopsp = T
        Instances For
          theorem Ctop.Realizer.eq {α : Type u_6} [T : TopologicalSpace α] (self : Ctop.Realizer α) :
          self.F.toTopsp = T
          def Ctop.toRealizer {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

          A Ctop realizes the topological space it generates.

          Equations
          • F.toRealizer = { σ := σ, F := F, eq := }
          Instances For
            instance instInhabitedRealizer {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :
            Equations
            theorem Ctop.Realizer.mem_nhds {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α} :
            s nhds a ∃ (b : F), a F.F.f b F.F.f b s
            theorem Ctop.Realizer.isOpen_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} :
            IsOpen s as, ∃ (b : F), a F.F.f b F.F.f b s
            theorem Ctop.Realizer.isClosed_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} :
            IsClosed s ∀ (a : α), (∀ (b : F), a F.F.f b∃ (z : α), z F.F.f b s)a s
            theorem Ctop.Realizer.mem_interior_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α} :
            a interior s ∃ (b : F), a F.F.f b F.F.f b s
            theorem Ctop.Realizer.isOpen {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (s : F) :
            IsOpen (F.F.f s)
            theorem Ctop.Realizer.ext' {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ} (H : ∀ (a : α) (s : Set α), s nhds a ∃ (b : σ), a F.f b F.f b s) :
            F.toTopsp = T
            theorem Ctop.Realizer.ext {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ} (H₁ : ∀ (a : σ), IsOpen (F.f a)) (H₂ : ∀ (a : α), snhds a, ∃ (b : σ), a F.f b F.f b s) :
            F.toTopsp = T

            The topological space realizer made of the open sets.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Ctop.Realizer.ofEquiv {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F τ) :

              Replace the representation type of a Ctop realizer.

              Equations
              Instances For
                @[simp]
                theorem Ctop.Realizer.ofEquiv_σ {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F τ) :
                (F.ofEquiv E) = τ
                @[simp]
                theorem Ctop.Realizer.ofEquiv_F {α : Type u_1} {τ : Type u_4} [TopologicalSpace α] (F : Ctop.Realizer α) (E : F τ) (s : τ) :
                (F.ofEquiv E).F.f s = F.F.f (E.symm s)
                def Ctop.Realizer.nhds {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) :
                (nhds a).Realizer

                A realizer of the neighborhood of a point.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Ctop.Realizer.nhds_σ {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) :
                  (F.nhds a) = { s : F // a F.F.f s }
                  @[simp]
                  theorem Ctop.Realizer.nhds_F {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) (s : (F.nhds a)) :
                  (F.nhds a).F.f s = F.F.f s
                  theorem Ctop.Realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {m : βα} {f : Filter β} (F : f.Realizer) (R : Ctop.Realizer α) {a : α} :
                  Filter.Tendsto m f (nhds a) ∀ (t : R), a R.F.f t∃ (s : F), xF.F.f s, m x R.F.f t
                  structure LocallyFinite.Realizer {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (F : Ctop.Realizer α) (f : βSet α) :
                  Type (max (max u_1 u_2) u_5)

                  A LocallyFinite.Realizer F f is a realization that f is locally finite, namely it is a choice of open sets from the basis of F such that they intersect only finitely many of the values of f.

                  • bas : (a : α) → { s : F // a F.F.f s }
                  • sets : (x : α) → Fintype {i : β | (f i F.F.f (self.bas x)).Nonempty}
                  Instances For
                    theorem LocallyFinite.Realizer.to_locallyFinite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {F : Ctop.Realizer α} {f : βSet α} (R : LocallyFinite.Realizer F f) :
                    instance instNonemptyRealizerOfFinite {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Finite β] (F : Ctop.Realizer α) (f : βSet α) :
                    Equations
                    • =
                    def Compact.Realizer {α : Type u_1} [TopologicalSpace α] (s : Set α) :
                    Type (max (max (max u_1 (u_5 + 1)) u_5) u_1)

                    A Compact.Realizer s is a realization that s is compact, namely it is a choice of finite open covers for each set family covering s.

                    Equations
                    Instances For
                      Equations
                      • instInhabitedRealizerEmptyCollectionSet = { default := fun {f : Filter α} (F : f.Realizer) (x : F) (h : f ) (hF : F.F.f x ) => let_fun this := ; absurd this h }