Documentation

Mathlib.Topology.Compactness.Lindelof

Lindelöf sets and Lindelöf spaces #

Main definitions #

We define the following properties for sets in a topological space:

Main results #

Implementation details #

def IsLindelof {X : Type u} [TopologicalSpace X] (s : Set X) :

A set s is Lindelöf if every nontrivial filter f with the countable intersection property that contains s, has a clusterpoint in s. The filter-free definition is given by isLindelof_iff_countable_subcover.

Equations
Instances For
    theorem IsLindelof.compl_mem_sets {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : xs, s nhds x f) :
    s f

    The complement to a Lindelöf set belongs to a filter f with the countable intersection property if it belongs to each filter 𝓝 x ⊓ f, x ∈ s.

    theorem IsLindelof.compl_mem_sets_of_nhdsWithin {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : xs, tnhdsWithin x s, t f) :
    s f

    The complement to a Lindelöf set belongs to a filter f with the countable intersection property if each x ∈ s has a neighborhood t within s such that tᶜ belongs to f.

    theorem IsLindelof.induction_on {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {p : Set XProp} (hmono : ∀ ⦃s t : Set X⦄, s tp tp s) (hcountable_union : ∀ (S : Set (Set X)), S.Countable(sS, p s)p (⋃₀ S)) (hnhds : xs, tnhdsWithin x s, p t) :
    p s

    If p : Set X → Prop is stable under restriction and union, and each point x of a Lindelöf set s has a neighborhood t within s such that p t, then p s holds.

    theorem IsLindelof.inter_right {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsClosed t) :

    The intersection of a Lindelöf set and a closed set is a Lindelöf set.

    theorem IsLindelof.inter_left {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (ht : IsLindelof t) (hs : IsClosed s) :

    The intersection of a closed set and a Lindelöf set is a Lindelöf set.

    theorem IsLindelof.diff {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsOpen t) :

    The set difference of a Lindelöf set and an open set is a Lindelöf set.

    theorem IsLindelof.of_isClosed_subset {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsClosed t) (h : t s) :

    A closed subset of a Lindelöf set is a Lindelöf set.

    theorem IsLindelof.image_of_continuousOn {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hs : IsLindelof s) (hf : ContinuousOn f s) :

    A continuous image of a Lindelöf set is a Lindelöf set.

    theorem IsLindelof.image {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hs : IsLindelof s) (hf : Continuous f) :

    A continuous image of a Lindelöf set is a Lindelöf set within the codomain.

    theorem IsLindelof.adherence_nhdset {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} {f : Filter X} [CountableInterFilter f] (hs : IsLindelof s) (hf₂ : f Filter.principal s) (ht₁ : IsOpen t) (ht₂ : xs, ClusterPt x fx t) :
    t f

    A filter with the countable intersection property that is finer than the principal filter on a Lindelöf set s contains any open set that contains all clusterpoints of s.

    theorem IsLindelof.elim_countable_subcover {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (U : ιSet X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
    ∃ (r : Set ι), r.Countable s ir, U i

    For every open cover of a Lindelöf set, there exists a countable subcover.

    theorem IsLindelof.elim_nhds_subcover' {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (U : (x : X) → x sSet X) (hU : ∀ (x : X) (hx : x s), U x hx nhds x) :
    ∃ (t : Set s), t.Countable s xt, U x
    theorem IsLindelof.elim_nhds_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (U : XSet X) (hU : xs, U x nhds x) :
    ∃ (t : Set X), t.Countable (xt, x s) s xt, U x
    theorem IsLindelof.indexed_countable_subcover {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι] (hs : IsLindelof s) (U : ιSet X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
    ∃ (f : ι), s ⋃ (n : ), U (f n)

    For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ.

    theorem IsLindelof.disjoint_nhdsSet_left {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) :
    Disjoint (nhdsSet s) l xs, Disjoint (nhds x) l

    The neighborhood filter of a Lindelöf set is disjoint with a filter l with the countable intersection property if and only if the neighborhood filter of each point of this set is disjoint with l.

    theorem IsLindelof.disjoint_nhdsSet_right {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) :
    Disjoint l (nhdsSet s) xs, Disjoint l (nhds x)

    A filter l with the countable intersection property is disjoint with the neighborhood filter of a Lindelöf set if and only if it is disjoint with the neighborhood filter of each point of this set.

    theorem IsLindelof.elim_countable_subfamily_closed {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ⋂ (i : ι), t i = ) :
    ∃ (u : Set ι), u.Countable s iu, t i =

    For every family of closed sets whose intersection avoids a Lindelö set, there exists a countable subfamily whose intersection avoids this Lindelöf set.

    theorem IsLindelof.inter_iInter_nonempty {X : Type u} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Set ι), u.Countable (s iu, t i).Nonempty) :
    (s ⋂ (i : ι), t i).Nonempty

    To show that a Lindelöf set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every countable subfamily.

    theorem IsLindelof.elim_countable_subcover_image {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ιSet X} (hs : IsLindelof s) (hc₁ : ib, IsOpen (c i)) (hc₂ : s ib, c i) :
    b'b, b'.Countable s ib', c i

    For every open cover of a Lindelöf set, there exists a countable subcover.

    theorem isLindelof_of_countable_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Set ι), t.Countable s it, U i) :

    A set s is Lindelöf if for every open cover of s, there exists a countable subcover.

    theorem isLindelof_of_countable_subfamily_closed {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable s iu, t i = ) :

    A set s is Lindelöf if for every family of closed sets whose intersection avoids s, there exists a countable subfamily whose intersection avoids s.

    theorem isLindelof_iff_countable_subcover {X : Type u} [TopologicalSpace X] {s : Set X} :
    IsLindelof s ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Set ι), t.Countable s it, U i

    A set s is Lindelöf if and only if for every open cover of s, there exists a countable subcover.

    theorem isLindelof_iff_countable_subfamily_closed {X : Type u} [TopologicalSpace X] {s : Set X} :
    IsLindelof s ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable s iu, t i =

    A set s is Lindelöf if and only if for every family of closed sets whose intersection avoids s, there exists a countable subfamily whose intersection avoids s.

    @[simp]

    The empty set is a Lindelof set.

    @[simp]
    theorem isLindelof_singleton {X : Type u} [TopologicalSpace X] {x : X} :

    A singleton set is a Lindelof set.

    theorem Set.Subsingleton.isLindelof {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Subsingleton) :
    theorem Set.Countable.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ιSet X} (hs : s.Countable) (hf : is, IsLindelof (f i)) :
    IsLindelof (is, f i)
    theorem Set.Finite.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ιSet X} (hs : s.Finite) (hf : is, IsLindelof (f i)) :
    IsLindelof (is, f i)
    theorem Finset.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] (s : Finset ι) {f : ιSet X} (hf : is, IsLindelof (f i)) :
    IsLindelof (is, f i)
    theorem isLindelof_accumulate {X : Type u} [TopologicalSpace X] {K : Set X} (hK : ∀ (n : ), IsLindelof (K n)) (n : ) :
    theorem Set.Countable.isLindelof_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : S.Countable) (hc : sS, IsLindelof s) :
    theorem Set.Finite.isLindelof_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : S.Finite) (hc : sS, IsLindelof s) :
    theorem isLindelof_iUnion {X : Type u} [TopologicalSpace X] {ι : Sort u_2} {f : ιSet X} [Countable ι] (h : ∀ (i : ι), IsLindelof (f i)) :
    IsLindelof (⋃ (i : ι), f i)
    theorem Set.Countable.isLindelof {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Countable) :
    theorem Set.Finite.isLindelof {X : Type u} [TopologicalSpace X] {s : Set X} (hs : s.Finite) :
    theorem IsLindelof.countable_of_discrete {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] (hs : IsLindelof s) :
    s.Countable
    theorem IsLindelof.union {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsLindelof t) :
    theorem IsLindelof.insert {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (a : X) :
    theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis {X : Type u} {ι : Type u_1} [TopologicalSpace X] (b : ιSet X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsLindelof (b i)) (U : Set X) :
    IsLindelof U IsOpen U ∃ (s : Set ι), s.Countable U = is, b i

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

    Filter.coLindelof is the filter generated by complements to Lindelöf sets.

    Equations
    Instances For
      theorem hasBasis_coLindelof {X : Type u} [TopologicalSpace X] :
      (Filter.coLindelof X).HasBasis IsLindelof compl
      theorem mem_coLindelof {X : Type u} [TopologicalSpace X] {s : Set X} :
      theorem mem_coLindelof' {X : Type u} [TopologicalSpace X] {s : Set X} :

      Filter.coclosedLindelof is the filter generated by complements to closed Lindelof sets.

      Equations
      Instances For
        theorem hasBasis_coclosedLindelof {X : Type u} [TopologicalSpace X] :
        (Filter.coclosedLindelof X).HasBasis (fun (s : Set X) => IsClosed s IsLindelof s) compl

        X is a Lindelöf space iff every open cover has a countable subcover.

        Instances

          In a Lindelöf space, Set.univ is a Lindelöf set.

          @[instance 10]
          Equations
          • =
          theorem cluster_point_of_Lindelof {X : Type u} [TopologicalSpace X] [LindelofSpace X] (f : Filter X) [f.NeBot] [CountableInterFilter f] :
          ∃ (x : X), ClusterPt x f
          theorem LindelofSpace.elim_nhds_subcover {X : Type u} [TopologicalSpace X] [LindelofSpace X] (U : XSet X) (hU : ∀ (x : X), U x nhds x) :
          ∃ (t : Set X), t.Countable xt, U x = Set.univ
          theorem lindelofSpace_of_countable_subfamily_closed {X : Type u} [TopologicalSpace X] (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable iu, t i = ) :
          theorem IsCompact.isLindelof {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) :

          A compact set s is Lindelöf.

          A σ-compact set s is Lindelöf

          @[instance 100]

          A compact space X is Lindelöf.

          Equations
          • =
          @[instance 100]

          A sigma-compact space X is Lindelöf.

          Equations
          • =

          X is a non-Lindelöf topological space if it is not a Lindelöf space.

          Instances

            In a non-Lindelöf space, Set.univ is not a Lindelöf set.

            theorem IsLindelof.ne_univ {X : Type u} [TopologicalSpace X] {s : Set X} [NonLindelofSpace X] (hs : IsLindelof s) :
            s Set.univ
            @[instance 100]

            A compact space X is Lindelöf.

            Equations
            • =
            theorem countable_cover_nhds_interior {X : Type u} [TopologicalSpace X] [LindelofSpace X] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
            ∃ (t : Set X), t.Countable xt, interior (U x) = Set.univ
            theorem countable_cover_nhds {X : Type u} [TopologicalSpace X] [LindelofSpace X] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
            ∃ (t : Set X), t.Countable xt, U x = Set.univ

            The comap of the coLindelöf filter on Y by a continuous function f : X → Y is less than or equal to the coLindelöf filter on X. This is a reformulation of the fact that images of Lindelöf sets are Lindelöf.

            theorem isLindelof_range {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [LindelofSpace X] {f : XY} (hf : Continuous f) :
            theorem Inducing.isLindelof_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hf : Inducing f) :

            If f : X → Y is an Inducing map, the image f '' s of a set s is Lindelöf if and only if s is compact.

            theorem Embedding.isLindelof_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hf : Embedding f) :

            If f : X → Y is an Embedding, the image f '' s of a set s is Lindelöf if and only if s is Lindelöf.

            theorem Inducing.isLindelof_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Inducing f) (hf' : IsClosed (Set.range f)) {K : Set Y} (hK : IsLindelof K) :

            The preimage of a Lindelöf set under an inducing map is a Lindelöf set.

            theorem ClosedEmbedding.isLindelof_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : ClosedEmbedding f) {K : Set Y} (hK : IsLindelof K) :

            The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.

            A closed embedding is proper, ie, inverse images of Lindelöf sets are contained in Lindelöf. Moreover, the preimage of a Lindelöf set is Lindelöf, see ClosedEmbedding.isLindelof_preimage.

            theorem Subtype.isLindelof_iff {X : Type u} [TopologicalSpace X] {p : XProp} {s : Set { x : X // p x }} :
            IsLindelof s IsLindelof (Subtype.val '' s)

            Sets of subtype are Lindelöf iff the image under a coercion is.

            theorem IsLindelof.countable {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (hs' : DiscreteTopology s) :
            s.Countable
            @[instance 100]

            Countable topological spaces are Lindelof.

            Equations
            • =

            The disjoint union of two Lindelöf spaces is Lindelöf.

            Equations
            • =
            instance instLindelofSpaceSigmaOfCountable {ι : Type u_1} {X : ιType u_2} [Countable ι] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LindelofSpace (X i)] :
            LindelofSpace ((i : ι) × X i)
            Equations
            • =
            instance Quot.LindelofSpace {X : Type u} [TopologicalSpace X] {r : XXProp} [LindelofSpace X] :
            Equations
            • =
            Equations
            • =

            A continuous image of a Lindelöf set is a Lindelöf set within the codomain.

            A set s is Hereditarily Lindelöf if every subset is a Lindelof set. We require this only for open sets in the definition, and then conclude that this holds for all sets by ADD.

            Equations
            Instances For

              Type class for Hereditarily Lindelöf spaces.

              Instances

                In a Hereditarily Lindelöf space, Set.univ is a Hereditarily Lindelöf set.

                @[instance 100]
                Equations
                • =
                theorem eq_open_union_countable {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u} (U : ιSet X) (h : ∀ (i : ι), IsOpen (U i)) :
                ∃ (t : Set ι), t.Countable it, U i = ⋃ (i : ι), U i
                Equations
                • =