Documentation

Mathlib.Topology.Sets.Opens

Open sets #

Summary #

We define the subtype of open sets in a topological space.

Main Definitions #

Bundled open sets #

Bundled open neighborhoods #

Main results #

We define order structures on both Opens α (CompleteLattice, Frame) and OpenNhdsOf x (OrderTop, DistribLattice).

TODO #

structure TopologicalSpace.Opens (α : Type u_2) [TopologicalSpace α] :
Type u_2

The type of open subsets of a topological space.

Instances For
    Equations
    • TopologicalSpace.Opens.instSetLike = { coe := TopologicalSpace.Opens.carrier, coe_injective' := }
    Equations
    • =
    theorem TopologicalSpace.Opens.forall {α : Type u_2} [TopologicalSpace α] {p : TopologicalSpace.Opens αProp} :
    (∀ (U : TopologicalSpace.Opens α), p U) ∀ (U : Set α) (hU : IsOpen U), p { carrier := U, is_open' := hU }
    @[simp]
    @[simp]
    theorem TopologicalSpace.Opens.coe_mk {α : Type u_2} [TopologicalSpace α] {U : Set α} {hU : IsOpen U} :
    { carrier := U, is_open' := hU } = U

    the coercion Opens α → Set α applied to a pair is the same as taking the first component

    @[simp]
    theorem TopologicalSpace.Opens.mem_mk {α : Type u_2} [TopologicalSpace α] {x : α} {U : Set α} {h : IsOpen U} :
    x { carrier := U, is_open' := h } x U
    theorem TopologicalSpace.Opens.nonempty_coe {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} :
    (U).Nonempty ∃ (x : α), x U
    theorem TopologicalSpace.Opens.ext {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} (h : U = V) :
    U = V
    @[simp]
    theorem TopologicalSpace.Opens.mk_coe {α : Type u_2} [TopologicalSpace α] (U : TopologicalSpace.Opens α) :
    { carrier := U, is_open' := } = U

    See Note [custom simps projection].

    Equations
    Instances For

      The interior of a set, as an element of Opens.

      Equations
      Instances For
        theorem TopologicalSpace.Opens.gc {α : Type u_2} [TopologicalSpace α] :
        GaloisConnection SetLike.coe TopologicalSpace.Opens.interior
        def TopologicalSpace.Opens.gi {α : Type u_2} [TopologicalSpace α] :
        GaloisCoinsertion SetLike.coe TopologicalSpace.Opens.interior

        The galois coinsertion between sets and opens.

        Equations
        • TopologicalSpace.Opens.gi = { choice := fun (s : Set α) (hs : s (TopologicalSpace.Opens.interior s)) => { carrier := s, is_open' := }, gc := , u_l_le := , choice_eq := }
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem TopologicalSpace.Opens.mk_inf_mk {α : Type u_2} [TopologicalSpace α] {U : Set α} {V : Set α} {hU : IsOpen U} {hV : IsOpen V} :
          { carrier := U, is_open' := hU } { carrier := V, is_open' := hV } = { carrier := U V, is_open' := }
          @[simp]
          theorem TopologicalSpace.Opens.coe_inf {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) (t : TopologicalSpace.Opens α) :
          (s t) = s t
          @[simp]
          theorem TopologicalSpace.Opens.coe_sup {α : Type u_2} [TopologicalSpace α] (s : TopologicalSpace.Opens α) (t : TopologicalSpace.Opens α) :
          (s t) = s t
          @[simp]
          theorem TopologicalSpace.Opens.mk_empty {α : Type u_2} [TopologicalSpace α] :
          { carrier := , is_open' := } =
          @[simp]
          theorem TopologicalSpace.Opens.mem_top {α : Type u_2} [TopologicalSpace α] (x : α) :
          @[simp]
          theorem TopologicalSpace.Opens.coe_top {α : Type u_2} [TopologicalSpace α] :
          = Set.univ
          @[simp]
          theorem TopologicalSpace.Opens.mk_univ {α : Type u_2} [TopologicalSpace α] :
          { carrier := Set.univ, is_open' := } =
          @[simp]
          theorem TopologicalSpace.Opens.coe_eq_univ {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} :
          U = Set.univ U =
          @[simp]
          theorem TopologicalSpace.Opens.coe_sSup {α : Type u_2} [TopologicalSpace α] {S : Set (TopologicalSpace.Opens α)} :
          (sSup S) = iS, i
          @[simp]
          theorem TopologicalSpace.Opens.coe_finset_sup {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ιTopologicalSpace.Opens α) (s : Finset ι) :
          (s.sup f) = s.sup (SetLike.coe f)
          @[simp]
          theorem TopologicalSpace.Opens.coe_finset_inf {ι : Type u_1} {α : Type u_2} [TopologicalSpace α] (f : ιTopologicalSpace.Opens α) (s : Finset ι) :
          (s.inf f) = s.inf (SetLike.coe f)
          Equations
          • TopologicalSpace.Opens.instInhabited = { default := }
          Equations
          • TopologicalSpace.Opens.instUniqueOfIsEmpty = { toInhabited := TopologicalSpace.Opens.instInhabited, uniq := }
          @[simp]
          theorem TopologicalSpace.Opens.coe_iSup {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} (s : ιTopologicalSpace.Opens α) :
          (⨆ (i : ι), s i) = ⋃ (i : ι), (s i)
          theorem TopologicalSpace.Opens.iSup_def {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} (s : ιTopologicalSpace.Opens α) :
          ⨆ (i : ι), s i = { carrier := ⋃ (i : ι), (s i), is_open' := }
          @[simp]
          theorem TopologicalSpace.Opens.iSup_mk {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} (s : ιSet α) (h : ∀ (i : ι), IsOpen (s i)) :
          ⨆ (i : ι), { carrier := s i, is_open' := } = { carrier := ⋃ (i : ι), s i, is_open' := }
          @[simp]
          theorem TopologicalSpace.Opens.mem_iSup {α : Type u_2} [TopologicalSpace α] {ι : Sort u_5} {x : α} {s : ιTopologicalSpace.Opens α} :
          x iSup s ∃ (i : ι), x s i
          @[simp]
          theorem TopologicalSpace.Opens.mem_sSup {α : Type u_2} [TopologicalSpace α] {Us : Set (TopologicalSpace.Opens α)} {x : α} :
          x sSup Us uUs, x u

          Open sets in a topological space form a frame.

          Equations
          Instances For
            Equations

            An open set in the indiscrete topology is either empty or the whole space.

            A set of opens α is a basis if the set of corresponding sets is a topological basis.

            Equations
            Instances For
              theorem TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion {α : Type u_2} [TopologicalSpace α] {ι : Type u_5} (b : ιTopologicalSpace.Opens α) (hb : TopologicalSpace.Opens.IsBasis (Set.range b)) (hb' : ∀ (i : ι), IsCompact (b i)) (U : Set α) :
              IsCompact U IsOpen U ∃ (s : Set ι), s.Finite U = is, (b i)

              If α has a basis consisting of compact opens, then an open set in α is compact open iff it is a finite union of some elements in the basis

              theorem TopologicalSpace.Opens.IsBasis.le_iff {α : Type u_5} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace α} {Us : Set (TopologicalSpace.Opens α)} (hUs : TopologicalSpace.Opens.IsBasis Us) :
              t₁ t₂ UUs, IsOpen U

              The preimage of an open set, as an open set.

              Equations
              Instances For
                @[simp]
                theorem TopologicalSpace.Opens.coe_comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (U : TopologicalSpace.Opens β) :
                theorem TopologicalSpace.Opens.comap_injective {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [T0Space β] :
                Function.Injective TopologicalSpace.Opens.comap
                @[simp]
                theorem Homeomorph.opensCongr_apply {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :
                f.opensCongr = (TopologicalSpace.Opens.comap f.symm.toContinuousMap)

                A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps.

                Equations
                Instances For
                  @[simp]
                  theorem Homeomorph.opensCongr_symm {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : α ≃ₜ β) :
                  f.opensCongr.symm = f.symm.opensCongr
                  structure TopologicalSpace.OpenNhdsOf {α : Type u_2} [TopologicalSpace α] (x : α) extends TopologicalSpace.Opens :
                  Type u_2

                  The open neighborhoods of a point. See also Opens or nhds.

                  Instances For
                    theorem TopologicalSpace.OpenNhdsOf.mem' {α : Type u_2} [TopologicalSpace α] {x : α} (self : TopologicalSpace.OpenNhdsOf x) :
                    x self.carrier

                    The point x belongs to every U : TopologicalSpace.OpenNhdsOf x.

                    theorem TopologicalSpace.OpenNhdsOf.toOpens_injective {α : Type u_2} [TopologicalSpace α] {x : α} :
                    Function.Injective TopologicalSpace.OpenNhdsOf.toOpens
                    Equations
                    instance TopologicalSpace.OpenNhdsOf.canLiftSet {α : Type u_2} [TopologicalSpace α] {x : α} :
                    CanLift (Set α) (TopologicalSpace.OpenNhdsOf x) SetLike.coe fun (s : Set α) => IsOpen s x s
                    Equations
                    • =
                    Equations
                    Equations
                    • TopologicalSpace.OpenNhdsOf.instInhabited = { default := }
                    Equations
                    Equations
                    Equations
                    • TopologicalSpace.OpenNhdsOf.instUniqueOfSubsingleton = { toInhabited := TopologicalSpace.OpenNhdsOf.instInhabited, uniq := }
                    Equations
                    theorem TopologicalSpace.OpenNhdsOf.basis_nhds {α : Type u_2} [TopologicalSpace α] {x : α} :
                    (nhds x).HasBasis (fun (x : TopologicalSpace.OpenNhdsOf x) => True) SetLike.coe

                    Preimage of an open neighborhood of f x under a continuous map f as a LatticeHom.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For