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.

Instances For
    instance instInhabitedCtopSet {α : Type u_1} :
    Inhabited (Ctop α (Set α))
    instance Ctop.instCoeFunCtopForAllSet {α : Type u_1} {σ : Type u_3} :
    CoeFun (Ctop α σ) fun x => σSet α
    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 : σ) :
    Ctop.f { f := f, top := T, top_mem := h₁, inter := I, inter_mem := h₂, inter_sub := h₃ } 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.

    Instances For
      @[simp]
      theorem Ctop.ofEquiv_val {α : Type u_1} {σ : Type u_3} {τ : Type u_4} (E : σ τ) (F : Ctop α σ) (a : τ) :
      Ctop.f (Ctop.ofEquiv E F) a = Ctop.f F (E.symm a)
      def Ctop.toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

      Every Ctop is a topological space.

      Instances For
        @[simp]
        theorem Ctop.mem_nhds_toTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) {s : Set α} {a : α} :
        s nhds a b, a Ctop.f F b Ctop.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.

        Instances For
          def Ctop.toRealizer {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :

          A Ctop realizes the topological space it generates.

          Instances For
            instance instInhabitedRealizerToTopsp {α : Type u_1} {σ : Type u_3} (F : Ctop α σ) :
            theorem Ctop.Realizer.mem_nhds {α : Type u_1} [T : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} {a : α} :
            s nhds a b, a Ctop.f F.F b Ctop.f F.F b s
            theorem Ctop.Realizer.isOpen_iff {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α} :
            IsOpen s ∀ (a : α), a sb, a Ctop.f F.F b Ctop.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 Ctop.f F.F bz, z Ctop.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, a Ctop.f F.F b Ctop.f F.F b s
            theorem Ctop.Realizer.isOpen {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (s : F) :
            IsOpen (Ctop.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 Ctop.f F b Ctop.f F b s) :
            theorem Ctop.Realizer.ext {α : Type u_1} [T : TopologicalSpace α] {σ : Type u_5} {F : Ctop α σ} (H₁ : ∀ (a : σ), IsOpen (Ctop.f F a)) (H₂ : ∀ (a : α) (s : Set α), s nhds ab, a Ctop.f F b Ctop.f F b s) :
            noncomputable def Ctop.Realizer.id {α : Type u_1} [TopologicalSpace α] :

            The topological space realizer made of the open sets.

            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.

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

                A realizer of the neighborhood of a point.

                Instances For
                  @[simp]
                  theorem Ctop.Realizer.nhds_σ {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) :
                  (Ctop.Realizer.nhds F a).σ = { s // a Ctop.f F.F s }
                  @[simp]
                  theorem Ctop.Realizer.nhds_F {α : Type u_1} [TopologicalSpace α] (F : Ctop.Realizer α) (a : α) (s : (Ctop.Realizer.nhds F a).σ) :
                  theorem Ctop.Realizer.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {m : βα} {f : Filter β} (F : Filter.Realizer f) (R : Ctop.Realizer α) {a : α} :
                  Filter.Tendsto m f (nhds a) ∀ (t : R), a Ctop.f R.F ts, ∀ (x : β), x CFilter.f F.F sm x Ctop.f R.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.

                  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 instNonemptyRealizer {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Finite β] (F : Ctop.Realizer α) (f : βSet α) :
                    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.

                    Instances For