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
    @[reducible, inline]
    abbrev TopologicalSpace.Opens.inclusion {α : Type u_2} [TopologicalSpace α] {U : TopologicalSpace.Opens α} {V : TopologicalSpace.Opens α} (h : U V) :
    UV

    A version of Set.inclusion not requiring definitional abuse

    Equations
    Instances For
      @[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 β) :
                  @[simp]
                  theorem TopologicalSpace.Opens.mem_comap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] {f : C(α, β)} {U : TopologicalSpace.Opens β} {x : α} :
                  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