doc-next-gen

Mathlib.Topology.Compactness.Lindelof

Module docstring

{"# Lindelöf sets and Lindelöf spaces

Main definitions

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

  • IsLindelof s: Two definitions are possible here. The more standard definition is that every open cover that contains s contains a countable subcover. We choose for the equivalent definition where we require that every nontrivial filter on s with the countable intersection property has a clusterpoint. Equivalence is established in isLindelof_iff_countable_subcover.
  • LindelofSpace X: X is Lindelöf if it is Lindelöf as a set.
  • NonLindelofSpace: a space that is not a Lindëlof space, e.g. the Long Line.

Main results

  • isLindelof_iff_countable_subcover: A set is Lindelöf iff every open cover has a countable subcover.

Implementation details

  • This API is mainly based on the API for IsCompact and follows notation and style as much as possible. "}
IsLindelof definition
(s : Set X)
Full source 
/-- 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`. -/
def IsLindelof (s : Set X) :=
  ∀ ⦃f⦄ [NeBot f] [CountableInterFilter f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
Lindelöf set
Informal description
A subset $s$ of a topological space $X$ is called Lindelöf if for every nontrivial filter $f$ on $X$ with the countable intersection property that contains $s$ (i.e., $f \leq \mathcal{P} s$), there exists a cluster point of $f$ in $s$. An equivalent characterization in terms of open covers is given by `isLindelof_iff_countable_subcover`.
IsLindelof.compl_mem_sets theorem
(hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) : sᶜ ∈ f
Full source 
/-- 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 (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f]
    (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) : sᶜsᶜ ∈ f := by
  contrapose! hf
  simp only [not_mem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
  exact hs inf_le_right
Complement of Lindelöf Set Belongs to Filter with Countable Intersection Property
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$, and let $f$ be a filter on $X$ with the countable intersection property. If for every $x \in s$, the complement $s^c$ belongs to the neighborhood filter $\mathcal{N}_x$ of $x$ intersected with $f$, then $s^c$ belongs to $f$.
IsLindelof.compl_mem_sets_of_nhdsWithin theorem
(hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f
Full source 
/-- 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.compl_mem_sets_of_nhdsWithin (hs : IsLindelof s) {f : Filter X}
    [CountableInterFilter f] (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜsᶜ ∈ f := by
  refine hs.compl_mem_sets fun x hx ↦ ?_
  rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]
  exact hf x hx
Complement of Lindelöf Set Belongs to Filter under Neighborhood Condition
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$, and let $f$ be a filter on $X$ with the countable intersection property. If for every $x \in s$, there exists a neighborhood $t$ of $x$ within $s$ such that the complement $t^c$ belongs to $f$, then the complement $s^c$ belongs to $f$.
IsLindelof.induction_on theorem
(hs : IsLindelof s) {p : Set X → Prop} (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s) (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S)) (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s
Full source 
/-- 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. -/
@[elab_as_elim]
theorem IsLindelof.induction_on (hs : IsLindelof s) {p : Set X → Prop}
    (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s)
    (hcountable_union : ∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p (⋃₀ S))
    (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s := by
  let f : Filter X := ofCountableUnion p hcountable_union (fun t ht _ hsub ↦ hmono hsub ht)
  have : sᶜsᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
  rwa [← compl_compl s]
Induction Principle for Lindelöf Sets
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$, and let $p$ be a property of subsets of $X$ such that: 1. (Monotonicity) If $s \subseteq t$ and $p(t)$ holds, then $p(s)$ holds. 2. (Countable union) For any countable family $\mathcal{S}$ of subsets of $X$, if $p(S)$ holds for every $S \in \mathcal{S}$, then $p(\bigcup \mathcal{S})$ holds. 3. (Local condition) For every $x \in s$, there exists a neighborhood $t$ of $x$ within $s$ such that $p(t)$ holds. Then $p(s)$ holds.
IsLindelof.inter_right theorem
(hs : IsLindelof s) (ht : IsClosed t) : IsLindelof (s ∩ t)
Full source 
/-- The intersection of a Lindelöf set and a closed set is a Lindelöf set. -/
theorem IsLindelof.inter_right (hs : IsLindelof s) (ht : IsClosed t) : IsLindelof (s ∩ t) := by
  intro f hnf _ hstf
  rw [← inf_principal, le_inf_iff] at hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f := hs hstf.1
  have hxt : x ∈ t := ht.mem_of_nhdsWithin_neBot <| hx.mono hstf.2
  exact ⟨x, ⟨hsx, hxt⟩, hx⟩
Intersection of Lindelöf Set with Closed Set is Lindelöf
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$ and $t$ be a closed subset of $X$. Then the intersection $s \cap t$ is also a Lindelöf set.
IsLindelof.inter_left theorem
(ht : IsLindelof t) (hs : IsClosed s) : IsLindelof (s ∩ t)
Full source 
/-- The intersection of a closed set and a Lindelöf set is a Lindelöf set. -/
theorem IsLindelof.inter_left (ht : IsLindelof t) (hs : IsClosed s) : IsLindelof (s ∩ t) :=
  inter_comm t s ▸ ht.inter_right hs
Intersection of Closed Set with Lindelöf Set is Lindelöf
Informal description
Let $t$ be a Lindelöf subset of a topological space $X$ and $s$ be a closed subset of $X$. Then the intersection $s \cap t$ is also a Lindelöf set.
IsLindelof.diff theorem
(hs : IsLindelof s) (ht : IsOpen t) : IsLindelof (s \ t)
Full source 
/-- The set difference of a Lindelöf set and an open set is a Lindelöf set. -/
theorem IsLindelof.diff (hs : IsLindelof s) (ht : IsOpen t) : IsLindelof (s \ t) :=
  hs.inter_right (isClosed_compl_iff.mpr ht)
Set Difference of Lindelöf Set and Open Set is Lindelöf
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$ and $t$ be an open subset of $X$. Then the set difference $s \setminus t$ is also a Lindelöf set.
IsLindelof.of_isClosed_subset theorem
(hs : IsLindelof s) (ht : IsClosed t) (h : t ⊆ s) : IsLindelof t
Full source 
/-- A closed subset of a Lindelöf set is a Lindelöf set. -/
theorem IsLindelof.of_isClosed_subset (hs : IsLindelof s) (ht : IsClosed t) (h : t ⊆ s) :
    IsLindelof t := inter_eq_self_of_subset_right h ▸ hs.inter_right ht
Closed Subset of Lindelöf Set is Lindelöf
Informal description
Let $s$ be a Lindelöf subset of a topological space $X$ and $t$ be a closed subset of $X$ such that $t \subseteq s$. Then $t$ is also a Lindelöf set.
IsLindelof.image_of_continuousOn theorem
{f : X → Y} (hs : IsLindelof s) (hf : ContinuousOn f s) : IsLindelof (f '' s)
Full source 
/-- A continuous image of a Lindelöf set is a Lindelöf set. -/
theorem IsLindelof.image_of_continuousOn {f : X → Y} (hs : IsLindelof s) (hf : ContinuousOn f s) :
    IsLindelof (f '' s) := by
  intro l lne _ ls
  have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
  obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this _ inf_le_right
  haveI := hx.neBot
  use f x, mem_image_of_mem f hxs
  have : Tendsto f (𝓝𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝𝓝 (f x) ⊓ l) := by
    convert (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
  exact this.neBot
Continuous Image of a Lindelöf Set is Lindelöf
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a Lindelöf subset, and $f \colon X \to Y$ a continuous function on $s$. Then the image $f(s)$ is a Lindelöf subset of $Y$.
IsLindelof.image theorem
{f : X → Y} (hs : IsLindelof s) (hf : Continuous f) : IsLindelof (f '' s)
Full source 
/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain. -/
theorem IsLindelof.image {f : X → Y} (hs : IsLindelof s) (hf : Continuous f) :
    IsLindelof (f '' s) := hs.image_of_continuousOn hf.continuousOn
Continuous Image of a Lindelöf Set is Lindelöf
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a Lindelöf subset, and $f \colon X \to Y$ a continuous function. Then the image $f(s)$ is a Lindelöf subset of $Y$.
IsLindelof.adherence_nhdset theorem
{f : Filter X} [CountableInterFilter f] (hs : IsLindelof s) (hf₂ : f ≤ 𝓟 s) (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f
Full source 
/-- 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.adherence_nhdset {f : Filter X} [CountableInterFilter f] (hs : IsLindelof s)
    (hf₂ : f ≤ 𝓟 s) (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f :=
  (eq_or_neBot _).casesOn mem_of_eq_bot fun _ ↦
    let ⟨x, hx, hfx⟩ := @hs (f ⊓ 𝓟 tᶜ) _ _ <| inf_le_of_left_le hf₂
    have : x ∈ t := ht₂ x hx hfx.of_inf_left
    have : tᶜtᶜ ∩ ttᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (ht₁.mem_nhds this)
    have A : 𝓝[tᶜ] x = ⊥ := empty_mem_iff_bot.1 <| compl_inter_self t ▸ this
    have : 𝓝[tᶜ] x𝓝[tᶜ] x ≠ ⊥ := hfx.of_inf_right.ne
    absurd A this
Lindelöf Set Property: Open Neighborhoods of Cluster Points Belong to Filter
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf set. For any filter $f$ on $X$ with the countable intersection property such that $f$ is finer than the principal filter on $s$, and for any open set $t \subseteq X$ containing all cluster points of $f$ in $s$, we have $t \in f$.
IsLindelof.elim_countable_subcover theorem
{ι : Type v} (hs : IsLindelof s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) : ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i)
Full source 
/-- For every open cover of a Lindelöf set, there exists a countable subcover. -/
theorem IsLindelof.elim_countable_subcover {ι : Type v} (hs : IsLindelof s) (U : ι → Set X)
    (hUo : ∀ i, IsOpen (U i)) (hsU : s ⊆ ⋃ i, U i) :
    ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i) := by
  have hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → (∃ r : Set ι, r.Countable ∧ t ⊆ ⋃ i ∈ r, U i)
      → (∃ r : Set ι, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i) := by
    intro _ _ hst ⟨r, ⟨hrcountable, hsub⟩⟩
    exact ⟨r, hrcountable, Subset.trans hst hsub⟩
  have hcountable_union : ∀ (S : Set (Set X)), S.Countable
      → (∀ s ∈ S, ∃ r : Set ι, r.Countable ∧ (s ⊆ ⋃ i ∈ r, U i))
      → ∃ r : Set ι, r.Countable ∧ (⋃₀ S ⊆ ⋃ i ∈ r, U i) := by
    intro S hS hsr
    choose! r hr using hsr
    refine ⟨⋃ s ∈ S, r s, hS.biUnion_iff.mpr (fun s hs ↦ (hr s hs).1), ?_⟩
    refine sUnion_subset ?h.right.h
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    exact fun i is x hx ↦ mem_biUnion is ((hr i is).2 hx)
  have h_nhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ r : Set ι, r.Countable ∧ (t ⊆ ⋃ i ∈ r, U i) := by
    intro x hx
    let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
    refine ⟨U i, mem_nhdsWithin_of_mem_nhds ((hUo i).mem_nhds hi), {i}, by simp, ?_⟩
    simp only [mem_singleton_iff, iUnion_iUnion_eq_left]
    exact Subset.refl _
  exact hs.induction_on hmono hcountable_union h_nhds
Lindelöf Sets Have Countable Subcovers
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. For any family of open sets $\{U_i\}_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$), there exists a countable subset $r \subseteq \iota$ such that $s \subseteq \bigcup_{i \in r} U_i$.
IsLindelof.elim_nhds_subcover' theorem
(hs : IsLindelof s) (U : ∀ x ∈ s, Set X) (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) : ∃ t : Set s, t.Countable ∧ s ⊆ ⋃ x ∈ t, U (x : s) x.2
Full source 
theorem IsLindelof.elim_nhds_subcover' (hs : IsLindelof s) (U : ∀ x ∈ s, Set X)
    (hU : ∀ x (hx : x ∈ s), U x ‹x ∈ s› ∈ 𝓝 x) :
    ∃ t : Set s, t.Countable ∧ s ⊆ ⋃ x ∈ t, U (x : s) x.2 := by
  have := hs.elim_countable_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦
      mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩
  rcases this with ⟨r, ⟨hr, hs⟩⟩
  use r, hr
  apply Subset.trans hs
  apply iUnion₂_subset
  intro i hi
  apply Subset.trans interior_subset
  exact subset_iUnion_of_subset i (subset_iUnion_of_subset hi (Subset.refl _))
Lindelöf Sets Have Countable Neighborhood Subcovers
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. For any family of neighborhoods $\{U_x\}_{x \in s}$ indexed by points in $s$ (i.e., for each $x \in s$, $U_x$ is a neighborhood of $x$), there exists a countable subset $t \subseteq s$ such that $s \subseteq \bigcup_{x \in t} U_x$.
IsLindelof.elim_nhds_subcover theorem
(hs : IsLindelof s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ 𝓝 x) : ∃ t : Set X, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
Full source 
theorem IsLindelof.elim_nhds_subcover (hs : IsLindelof s) (U : X → Set X)
    (hU : ∀ x ∈ s, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x := by
  let ⟨t, ⟨htc, htsub⟩⟩ := hs.elim_nhds_subcover' (fun x _ ↦ U x) hU
  refine ⟨↑t, Countable.image htc Subtype.val, ?_⟩
  constructor
  · intro _
    simp only [mem_image, Subtype.exists, exists_and_right, exists_eq_right, forall_exists_index]
    tauto
  · have : ⋃ x ∈ t, U ↑x = ⋃ x ∈ Subtype.val '' t, U x := biUnion_image.symm
    rwa [← this]
Existence of Countable Neighborhood Subcover for Lindelöf Sets
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. For any function $U : X \to \text{Set } X$ such that for every $x \in s$, $U(x)$ is a neighborhood of $x$, there exists a countable subset $t \subseteq X$ satisfying: 1. Every element of $t$ belongs to $s$ (i.e., $\forall x \in t, x \in s$), 2. $s$ is covered by the union of $U(x)$ over $x \in t$ (i.e., $s \subseteq \bigcup_{x \in t} U(x)$).
IsLindelof.indexed_countable_subcover theorem
{ι : 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)
Full source 
/-- For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ. -/
theorem IsLindelof.indexed_countable_subcover {ι : 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) := by
  obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU
  rcases c.eq_empty_or_nonempty with rfl | c_nonempty
  · simp only [mem_empty_iff_false, iUnion_of_empty, iUnion_empty] at c_cov
    simp only [subset_eq_empty c_cov rfl, empty_subset, exists_const]
  obtain ⟨f, f_surj⟩ := (Set.countable_iff_exists_surjective c_nonempty).mp c_count
  refine ⟨fun x ↦ f x, c_cov.trans <| iUnion₂_subset_iff.mpr (?_ : ∀ i ∈ c, U i ⊆ ⋃ n, U (f n))⟩
  intro x hx
  obtain ⟨n, hn⟩ := f_surj ⟨x, hx⟩
  exact subset_iUnion_of_subset n <| subset_of_eq (by rw [hn])
Existence of Countably Indexed Subcover for Lindelöf Sets
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. Given a nonempty index set $\iota$ and a family of open sets $\{U_i\}_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$), there exists a sequence $(f(n))_{n \in \mathbb{N}}$ in $\iota$ such that $s \subseteq \bigcup_{n \in \mathbb{N}} U_{f(n)}$.
IsLindelof.disjoint_nhdsSet_left theorem
{l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) : Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l
Full source 
/-- 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_left {l : Filter X} [CountableInterFilter l]
    (hs : IsLindelof s) :
    DisjointDisjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l := by
  refine ⟨fun h x hx ↦ h.mono_left <| nhds_le_nhdsSet hx, fun H ↦ ?_⟩
  choose! U hxU hUl using fun x hx ↦ (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
  choose hxU hUo using hxU
  rcases hs.elim_nhds_subcover U fun x hx ↦ (hUo x hx).mem_nhds (hxU x hx) with ⟨t, htc, hts, hst⟩
  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx ↦ hUo x (hts x hx), hst⟩, ?_⟩
  rw [compl_iUnion₂]
  exact (countable_bInter_mem htc).mpr (fun i hi ↦ hUl _ (hts _ hi))
Disjointness of Lindelöf Set's Neighborhood Filter with Countable Intersection Filter
Informal description
Let $X$ be a topological space, $s \subseteq X$ a Lindelöf subset, and $l$ a filter on $X$ with the countable intersection property. Then the neighborhood filter of $s$ is disjoint with $l$ if and only if for every $x \in s$, the neighborhood filter of $x$ is disjoint with $l$.
IsLindelof.disjoint_nhdsSet_right theorem
{l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) : Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
Full source 
/-- 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.disjoint_nhdsSet_right {l : Filter X} [CountableInterFilter l]
    (hs : IsLindelof s) : DisjointDisjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x) := by
  simpa only [disjoint_comm] using hs.disjoint_nhdsSet_left
Disjointness of Filter with Lindelöf Set's Neighborhood Filter via Pointwise Disjointness
Informal description
Let $X$ be a topological space, $s \subseteq X$ a Lindelöf subset, and $l$ a filter on $X$ with the countable intersection property. Then $l$ is disjoint with the neighborhood filter of $s$ if and only if for every $x \in s$, $l$ is disjoint with the neighborhood filter of $x$.
IsLindelof.elim_countable_subfamily_closed theorem
{ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅) : ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅
Full source 
/-- 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.elim_countable_subfamily_closed {ι : Type v} (hs : IsLindelof s)
    (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : (s ∩ ⋂ i, t i) = ∅) :
    ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅ := by
  let U := tᶜ
  have hUo : ∀ i, IsOpen (U i) := by simp only [U, Pi.compl_apply, isOpen_compl_iff]; exact htc
  have hsU : s ⊆ ⋃ i, U i := by
    simp only [U, Pi.compl_apply]
    rw [← compl_iInter]
    apply disjoint_compl_left_iff_subset.mp
    simp only [compl_iInter, compl_iUnion, compl_compl]
    apply Disjoint.symm
    exact disjoint_iff_inter_eq_empty.mpr hst
  rcases hs.elim_countable_subcover U hUo hsU with ⟨u, ⟨hucount, husub⟩⟩
  use u, hucount
  rw [← disjoint_compl_left_iff_subset] at husub
  simp only [U, Pi.compl_apply, compl_iUnion, compl_compl] at husub
  exact disjoint_iff_inter_eq_empty.mp (Disjoint.symm husub)
Lindelöf Sets Have Countable Subfamilies of Closed Sets with Empty Intersection
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. Given a family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i \in \iota} t_i = \emptyset$, there exists a countable subset $u \subseteq \iota$ such that $s \cap \bigcap_{i \in u} t_i = \emptyset$.
IsLindelof.inter_iInter_nonempty theorem
{ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i)) (hst : ∀ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ i, t i).Nonempty
Full source 
/-- 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.inter_iInter_nonempty {ι : Type v} (hs : IsLindelof s) (t : ι → Set X)
    (htc : ∀ i, IsClosed (t i)) (hst : ∀ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) :
    (s ∩ ⋂ i, t i).Nonempty := by
  contrapose! hst
  rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩
  exact ⟨u, fun _ ↦ husub⟩
Nonempty Intersection of Lindelöf Set with Closed Family Having Countable Intersection Property
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. Given a family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that for every countable subset $u \subseteq \iota$, the intersection $s \cap \bigcap_{i \in u} t_i$ is nonempty, then the intersection $s \cap \bigcap_{i \in \iota} t_i$ is also nonempty.
IsLindelof.elim_countable_subcover_image theorem
{b : Set ι} {c : ι → Set X} (hs : IsLindelof s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b', b' ⊆ b ∧ Set.Countable b' ∧ s ⊆ ⋃ i ∈ b', c i
Full source 
/-- For every open cover of a Lindelöf set, there exists a countable subcover. -/
theorem IsLindelof.elim_countable_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsLindelof s)
    (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) :
    ∃ b', b' ⊆ b ∧ Set.Countable b' ∧ s ⊆ ⋃ i ∈ b', c i := by
  simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
  rcases hs.elim_countable_subcover (fun i ↦ c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
  refine ⟨Subtype.val '' d, by simp, Countable.image hd.1 Subtype.val, ?_⟩
  rw [biUnion_image]
  exact hd.2
Lindelöf Sets Have Countable Subcovers from Indexed Families
Informal description
Let $X$ be a topological space and $s \subseteq X$ a Lindelöf subset. Given an index set $b$ and a family of open sets $\{c_i\}_{i \in b}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in b} c_i$), there exists a countable subset $b' \subseteq b$ such that $\{c_i\}_{i \in b'}$ still covers $s$ (i.e., $s \subseteq \bigcup_{i \in b'} c_i$).
isLindelof_of_countable_subcover theorem
(h : ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) : IsLindelof s
Full source 
/-- A set `s` is Lindelöf if for every open cover of `s`, there exists a countable subcover. -/
theorem isLindelof_of_countable_subcover
    (h : ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) →
    ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) :
    IsLindelof s := fun f hf hfs ↦ by
  contrapose! h
  simp only [ClusterPt, not_neBot, ← disjoint_iff, SetCoe.forall',
    (nhds_basis_opens _).disjoint_iff_left] at h
  choose fsub U hU hUf using h
  refine ⟨s, U, fun x ↦ (hU x).2, fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, (hU _).1 ⟩, ?_⟩
  intro t ht h
  have uinf := f.sets_of_superset (le_principal_iff.1 fsub) h
  have uninf : ⋂ i ∈ t, (U i)ᶜ⋂ i ∈ t, (U i)ᶜ ∈ f := (countable_bInter_mem ht).mpr (fun _ _ ↦ hUf _)
  rw [← compl_iUnion₂] at uninf
  have uninf := compl_not_mem uninf
  simp only [compl_compl] at uninf
  contradiction
Characterization of Lindelöf Sets via Countable Subcovers
Informal description
A subset $s$ of a topological space $X$ is Lindelöf if for every family of open sets $\{U_i\}_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i} U_i$), there exists a countable subset $\iota' \subseteq \iota$ such that $\{U_i\}_{i \in \iota'}$ still covers $s$ (i.e., $s \subseteq \bigcup_{i \in \iota'} U_i$).
isLindelof_of_countable_subfamily_closed theorem
(h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅) : IsLindelof s
Full source 
/-- 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_of_countable_subfamily_closed
    (h :
      ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ →
        ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅) :
    IsLindelof s :=
  isLindelof_of_countable_subcover fun U hUo hsU ↦ by
    rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
    rcases h (fun i ↦ (U i)ᶜ) (fun i ↦ (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
    refine ⟨t, ?_⟩
    rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]
Lindelöf Property via Countable Subfamilies of Closed Sets
Informal description
A subset $s$ of a topological space $X$ is Lindelöf if for every family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i} t_i = \emptyset$, there exists a countable subset $\iota' \subseteq \iota$ such that $s \cap \bigcap_{i \in \iota'} t_i = \emptyset$.
isLindelof_iff_countable_subcover theorem
: IsLindelof s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
Full source 
/-- 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_subcover :
    IsLindelofIsLindelof s ↔ ∀ {ι : Type u} (U : ι → Set X),
      (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Set ι, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i :=
  ⟨fun hs ↦ hs.elim_countable_subcover, isLindelof_of_countable_subcover⟩
Characterization of Lindelöf Sets via Countable Subcovers
Informal description
A subset $s$ of a topological space $X$ is Lindelöf if and only if for every family of open sets $\{U_i\}_{i \in \iota}$ covering $s$ (i.e., $s \subseteq \bigcup_{i \in \iota} U_i$), there exists a countable subset $\iota' \subseteq \iota$ such that $\{U_i\}_{i \in \iota'}$ still covers $s$ (i.e., $s \subseteq \bigcup_{i \in \iota'} U_i$).
isLindelof_iff_countable_subfamily_closed theorem
: IsLindelof s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅
Full source 
/-- 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`. -/
theorem isLindelof_iff_countable_subfamily_closed :
    IsLindelofIsLindelof s ↔ ∀ {ι : Type u} (t : ι → Set X),
    (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅
    → ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅ :=
  ⟨fun hs ↦ hs.elim_countable_subfamily_closed, isLindelof_of_countable_subfamily_closed⟩
Characterization of Lindelöf Sets via Countable Subfamilies of Closed Sets
Informal description
A subset $s$ of a topological space $X$ is Lindelöf if and only if for every family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ such that $s \cap \bigcap_{i} t_i = \emptyset$, there exists a countable subset $u \subseteq \iota$ such that $s \cap \bigcap_{i \in u} t_i = \emptyset$.
Set.Countable.isLindelof_biUnion theorem
{s : Set ι} {f : ι → Set X} (hs : s.Countable) (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)
Full source 
theorem Set.Countable.isLindelof_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Countable)
    (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i) := by
  apply isLindelof_of_countable_subcover
  intro i U hU hUcover
  have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i :=
    fun _ is ↦ _root_.subset_trans (subset_biUnion_of_mem is) hUcover
  have iSets := fun i is ↦ (hf i is).elim_countable_subcover U hU (hiU i is)
  choose! r hr using iSets
  use ⋃ i ∈ s, r i
  constructor
  · refine (Countable.biUnion_iff hs).mpr ?h.left.a
    exact fun s hs ↦ (hr s hs).1
  · refine iUnion₂_subset ?h.right.h
    intro i is
    simp only [mem_iUnion, exists_prop, iUnion_exists, biUnion_and']
    intro x hx
    exact mem_biUnion is ((hr i is).2 hx)
Countable Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space, $\iota$ an index set, and $s \subseteq \iota$ a countable subset. If for each $i \in s$, the set $f(i) \subseteq X$ is Lindelöf, then the union $\bigcup_{i \in s} f(i)$ is also Lindelöf.
Set.Finite.isLindelof_biUnion theorem
{s : Set ι} {f : ι → Set X} (hs : s.Finite) (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)
Full source 
theorem Set.Finite.isLindelof_biUnion {s : Set ι} {f : ι → Set X} (hs : s.Finite)
    (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i) :=
  Set.Countable.isLindelof_biUnion (countable hs) hf
Finite Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space, $\iota$ an index set, and $s \subseteq \iota$ a finite subset. If for each $i \in s$, the set $f(i) \subseteq X$ is Lindelöf, then the union $\bigcup_{i \in s} f(i)$ is also Lindelöf.
Finset.isLindelof_biUnion theorem
(s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)
Full source 
theorem Finset.isLindelof_biUnion (s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsLindelof (f i)) :
    IsLindelof (⋃ i ∈ s, f i) :=
  s.finite_toSet.isLindelof_biUnion hf
Finite Union of Lindelöf Sets is Lindelöf (Finset Version)
Informal description
Let $X$ be a topological space, $\iota$ an index type, and $s$ a finite subset of $\iota$ (represented as a `Finset`). If for each $i \in s$, the set $f(i) \subseteq X$ is Lindelöf, then the union $\bigcup_{i \in s} f(i)$ is also Lindelöf.
isLindelof_accumulate theorem
{K : ℕ → Set X} (hK : ∀ n, IsLindelof (K n)) (n : ℕ) : IsLindelof (Accumulate K n)
Full source 
theorem isLindelof_accumulate {K : ℕ → Set X} (hK : ∀ n, IsLindelof (K n)) (n : ℕ) :
    IsLindelof (Accumulate K n) :=
  (finite_le_nat n).isLindelof_biUnion fun k _ => hK k
Accumulated Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space and $K \colon \mathbb{N} \to \text{Set } X$ a sequence of subsets of $X$. If for every natural number $n$, the set $K(n)$ is Lindelöf, then for any $n \in \mathbb{N}$, the accumulated union $\text{Accumulate } K \, n$ is also Lindelöf.
Set.Countable.isLindelof_sUnion theorem
{S : Set (Set X)} (hf : S.Countable) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)
Full source 
theorem Set.Countable.isLindelof_sUnion {S : Set (Set X)} (hf : S.Countable)
    (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isLindelof_biUnion hc
Countable Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space and $S$ a countable family of subsets of $X$. If every set $s \in S$ is Lindelöf, then the union $\bigcup S$ is also Lindelöf.
Set.Finite.isLindelof_sUnion theorem
{S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)
Full source 
theorem Set.Finite.isLindelof_sUnion {S : Set (Set X)} (hf : S.Finite)
    (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isLindelof_biUnion hc
Finite Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space and $S$ a finite collection of subsets of $X$. If every set $s \in S$ is Lindelöf, then the union $\bigcup S$ is also Lindelöf.
isLindelof_iUnion theorem
{ι : Sort*} {f : ι → Set X} [Countable ι] (h : ∀ i, IsLindelof (f i)) : IsLindelof (⋃ i, f i)
Full source 
theorem isLindelof_iUnion {ι : Sort*} {f : ι → Set X} [Countable ι] (h : ∀ i, IsLindelof (f i)) :
    IsLindelof (⋃ i, f i) := (countable_range f).isLindelof_sUnion  <| forall_mem_range.2 h
Countable Union of Lindelöf Sets is Lindelöf
Informal description
Let $X$ be a topological space and $\{f_i\}_{i \in \iota}$ a countable family of subsets of $X$ indexed by a countable type $\iota$. If each $f_i$ is Lindelöf, then their union $\bigcup_{i \in \iota} f_i$ is also Lindelöf.
IsLindelof.countable_of_discrete theorem
[DiscreteTopology X] (hs : IsLindelof s) : s.Countable
Full source 
theorem IsLindelof.countable_of_discrete [DiscreteTopology X] (hs : IsLindelof s) :
    s.Countable := by
  have : ∀ x : X, ({x} : Set X) ∈ 𝓝 x := by simp [nhds_discrete]
  rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, ht, _, hssubt⟩
  rw [biUnion_of_singleton] at hssubt
  exact ht.mono hssubt
Countability of Lindelöf Sets in Discrete Spaces
Informal description
Let $X$ be a topological space with the discrete topology. If a subset $s \subseteq X$ is Lindelöf, then $s$ is countable.
IsLindelof.union theorem
(hs : IsLindelof s) (ht : IsLindelof t) : IsLindelof (s ∪ t)
Full source 
theorem IsLindelof.union (hs : IsLindelof s) (ht : IsLindelof t) : IsLindelof (s ∪ t) := by
  rw [union_eq_iUnion]; exact isLindelof_iUnion fun b => by cases b <;> assumption
Union of Lindelöf Sets is Lindelöf
Informal description
If $s$ and $t$ are Lindelöf subsets of a topological space $X$, then their union $s \cup t$ is also Lindelöf.
IsLindelof.insert theorem
(hs : IsLindelof s) (a) : IsLindelof (insert a s)
Full source 
protected theorem IsLindelof.insert (hs : IsLindelof s) (a) : IsLindelof (insert a s) :=
  isLindelof_singleton.union hs
Insertion Preserves Lindelöf Property
Informal description
If $s$ is a Lindelöf subset of a topological space $X$ and $a$ is any point in $X$, then the set obtained by inserting $a$ into $s$ (i.e., $s \cup \{a\}$) is also Lindelöf.
isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis theorem
(b : ι → Set X) (hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsLindelof (b i)) (U : Set X) : IsLindelof U ∧ IsOpen U ↔ ∃ s : Set ι, s.Countable ∧ U = ⋃ i ∈ s, b i
Full source 
/-- 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 -/
theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis (b : ι → Set X)
    (hb : IsTopologicalBasis (Set.range b)) (hb' : ∀ i, IsLindelof (b i)) (U : Set X) :
    IsLindelofIsLindelof U ∧ IsOpen UIsLindelof U ∧ IsOpen U ↔ ∃ s : Set ι, s.Countable ∧ U = ⋃ i ∈ s, b i := by
  constructor
  · rintro ⟨h₁, h₂⟩
    obtain ⟨Y, f, rfl, hf⟩ := hb.open_eq_iUnion h₂
    choose f' hf' using hf
    have : b ∘ f' = f := funext hf'
    subst this
    obtain ⟨t, ht⟩ :=
      h₁.elim_countable_subcover (b ∘ f') (fun i => hb.isOpen (Set.mem_range_self _)) Subset.rfl
    refine ⟨t.image f', Countable.image (ht.1) f', le_antisymm ?_ ?_⟩
    · refine Set.Subset.trans ht.2 ?_
      simp only [Set.iUnion_subset_iff]
      intro i hi
      rw [← Set.iUnion_subtype (fun x : ι => x ∈ t.image f') fun i => b i.1]
      exact Set.subset_iUnion (fun i : t.image f' => b i) ⟨_, mem_image_of_mem _ hi⟩
    · apply Set.iUnion₂_subset
      rintro i hi
      obtain ⟨j, -, rfl⟩ := (mem_image ..).mp hi
      exact Set.subset_iUnion (b ∘ f') j
  · rintro ⟨s, hs, rfl⟩
    constructor
    · exact hs.isLindelof_biUnion fun i _ => hb' i
    · exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)
Characterization of Lindelöf Open Sets via Countable Basis Unions
Informal description
Let $X$ be a topological space with a basis $\{b_i\}_{i \in \iota}$ consisting of Lindelöf open sets. Then, for any open set $U \subseteq X$, the following are equivalent: 1. $U$ is Lindelöf and open. 2. There exists a countable subset $s \subseteq \iota$ such that $U = \bigcup_{i \in s} b_i$.
Filter.coLindelof definition
(X : Type*) [TopologicalSpace X] : Filter X
Full source 
/-- `Filter.coLindelof` is the filter generated by complements to Lindelöf sets. -/
def Filter.coLindelof (X : Type*) [TopologicalSpace X] : Filter X :=
  --`Filter.coLindelof` is the filter generated by complements to Lindelöf sets.
  ⨅ (s : Set X) (_ : IsLindelof s), 𝓟 sᶜ
Cofilter of Lindelöf sets
Informal description
The filter `Filter.coLindelof` on a topological space $X$ is defined as the infimum of the principal filters generated by the complements of all Lindelöf subsets of $X$. In other words, it is the filter consisting of all subsets of $X$ that contain the complement of some Lindelöf subset of $X$.
hasBasis_coLindelof theorem
: (coLindelof X).HasBasis IsLindelof compl
Full source 
theorem hasBasis_coLindelof : (coLindelof X).HasBasis IsLindelof compl :=
  hasBasis_biInf_principal'
    (fun s hs t ht =>
      ⟨s ∪ t, hs.union ht, compl_subset_compl.2 subset_union_left,
        compl_subset_compl.2 subset_union_right⟩)
    ⟨∅, isLindelof_empty⟩
Basis Characterization of the Co-Lindelöf Filter
Informal description
The co-Lindelöf filter on a topological space $X$ has a basis consisting of the complements of all Lindelöf subsets of $X$. That is, a set $s$ is in the co-Lindelöf filter if and only if it contains the complement of some Lindelöf subset of $X$.
mem_coLindelof theorem
: s ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ tᶜ ⊆ s
Full source 
theorem mem_coLindelof : s ∈ coLindelof Xs ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ tᶜ ⊆ s :=
  hasBasis_coLindelof.mem_iff
Characterization of Membership in the Co-Lindelöf Filter
Informal description
A subset $s$ of a topological space $X$ belongs to the co-Lindelöf filter if and only if there exists a Lindelöf subset $t$ of $X$ such that the complement of $t$ is contained in $s$. In other words, $s \in \text{coLindelof}(X) \leftrightarrow \exists t, \text{IsLindelof}(t) \land t^c \subseteq s$.
mem_coLindelof' theorem
: s ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ sᶜ ⊆ t
Full source 
theorem mem_coLindelof' : s ∈ coLindelof Xs ∈ coLindelof X ↔ ∃ t, IsLindelof t ∧ sᶜ ⊆ t :=
  mem_coLindelof.trans <| exists_congr fun _ => and_congr_right fun _ => compl_subset_comm
Characterization of Membership in the Co-Lindelöf Filter via Complement Containment
Informal description
A subset $s$ of a topological space $X$ belongs to the co-Lindelöf filter if and only if there exists a Lindelöf subset $t$ of $X$ such that the complement of $s$ is contained in $t$. In other words, $s \in \text{coLindelof}(X) \leftrightarrow \exists t, \text{IsLindelof}(t) \land s^c \subseteq t$.
coLindelof_le_cofinite theorem
: coLindelof X ≤ cofinite
Full source 
theorem coLindelof_le_cofinite : coLindelof X ≤ cofinite := fun s hs =>
  compl_compl s ▸ hs.isLindelof.compl_mem_coLindelof
Cofinite Filter is Coarser than Co-Lindelöf Filter
Informal description
For any topological space $X$, the co-Lindelöf filter on $X$ is finer than the cofinite filter on $X$. In other words, every set in the co-Lindelöf filter is also in the cofinite filter.
Tendsto.isLindelof_insert_range_of_coLindelof theorem
{f : X → Y} {y} (hf : Tendsto f (coLindelof X) (𝓝 y)) (hfc : Continuous f) : IsLindelof (insert y (range f))
Full source 
theorem Tendsto.isLindelof_insert_range_of_coLindelof {f : X → Y} {y}
    (hf : Tendsto f (coLindelof X) (𝓝 y)) (hfc : Continuous f) :
    IsLindelof (insert y (range f)) := by
  intro l hne _ hle
  by_cases hy : ClusterPt y l
  · exact ⟨y, Or.inl rfl, hy⟩
  simp only [clusterPt_iff_nonempty, not_forall, ← not_disjoint_iff_nonempty_inter, not_not] at hy
  rcases hy with ⟨s, hsy, t, htl, hd⟩
  rcases mem_coLindelof.1 (hf hsy) with ⟨K, hKc, hKs⟩
  have : f '' Kf '' K ∈ l := by
    filter_upwards [htl, le_principal_iff.1 hle] with y hyt hyf
    rcases hyf with (rfl | ⟨x, rfl⟩)
    exacts [(hd.le_bot ⟨mem_of_mem_nhds hsy, hyt⟩).elim,
      mem_image_of_mem _ (not_not.1 fun hxK => hd.le_bot ⟨hKs hxK, hyt⟩)]
  rcases hKc.image hfc (le_principal_iff.2 this) with ⟨y, hy, hyl⟩
  exact ⟨y, Or.inr <| image_subset_range _ _ hy, hyl⟩
Lindelöfness of Extended Range under Co-Lindelöf Convergence
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, and $y \in Y$. If $f$ tends to $y$ along the co-Lindelöf filter of $X$, then the set $\{y\} \cup f(X)$ is Lindelöf in $Y$.
Filter.coclosedLindelof definition
(X : Type*) [TopologicalSpace X] : Filter X
Full source 
/-- `Filter.coclosedLindelof` is the filter generated by complements to closed Lindelof sets. -/
def Filter.coclosedLindelof (X : Type*) [TopologicalSpace X] : Filter X :=
  -- `Filter.coclosedLindelof` is the filter generated by complements to closed Lindelof sets.
  ⨅ (s : Set X) (_ : IsClosed s) (_ : IsLindelof s), 𝓟 sᶜ
Filter of complements of closed Lindelöf sets
Informal description
The filter `Filter.coclosedLindelof X` on a topological space $X$ is defined as the infimum of all principal filters generated by the complements of closed Lindelöf subsets of $X$. In other words, it is the filter consisting of all subsets of $X$ that contain the complement of some closed Lindelöf set.
hasBasis_coclosedLindelof theorem
: (Filter.coclosedLindelof X).HasBasis (fun s => IsClosed s ∧ IsLindelof s) compl
Full source 
theorem hasBasis_coclosedLindelof :
    (Filter.coclosedLindelof X).HasBasis (fun s => IsClosedIsClosed s ∧ IsLindelof s) compl := by
  simp only [Filter.coclosedLindelof, iInf_and']
  refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isLindelof_empty⟩
  rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
  exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩
Basis Characterization of Coclosed Lindelöf Filter
Informal description
The filter of complements of closed Lindelöf sets in a topological space $X$ has a basis consisting of the complements of all closed Lindelöf subsets of $X$. That is, a set $s$ is in the filter $\text{coclosedLindelof}\, X$ if and only if there exists a closed Lindelöf subset $t$ of $X$ such that $s = t^c$.
mem_coclosedLindelof theorem
: s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s
Full source 
theorem mem_coclosedLindelof : s ∈ coclosedLindelof Xs ∈ coclosedLindelof X ↔
    ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s := by
  simp only [hasBasis_coclosedLindelof.mem_iff, and_assoc]
Characterization of Membership in Coclosed Lindelöf Filter via Complements
Informal description
A subset $s$ of a topological space $X$ belongs to the filter $\text{coclosedLindelof}\, X$ if and only if there exists a closed Lindelöf subset $t$ of $X$ such that the complement of $t$ is contained in $s$. In other words, $s \in \text{coclosedLindelof}\, X$ if and only if $\exists t \subseteq X$, where $t$ is closed and Lindelöf, and $t^c \subseteq s$.
mem_coclosed_Lindelof' theorem
: s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t
Full source 
theorem mem_coclosed_Lindelof' : s ∈ coclosedLindelof Xs ∈ coclosedLindelof X ↔
    ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t := by
  simp only [mem_coclosedLindelof, compl_subset_comm]
Characterization of Membership in Coclosed Lindelöf Filter
Informal description
A subset $s$ of a topological space $X$ belongs to the filter of complements of closed Lindelöf sets if and only if there exists a closed Lindelöf subset $t$ of $X$ such that the complement of $s$ is contained in $t$. In other words, $s \in \text{coclosedLindelof}\, X \leftrightarrow \exists t, \text{IsClosed}\, t \land \text{IsLindelof}\, t \land s^c \subseteq t$.
coLindelof_le_coclosedLindelof theorem
: coLindelof X ≤ coclosedLindelof X
Full source 
theorem coLindelof_le_coclosedLindelof : coLindelof X ≤ coclosedLindelof X :=
  iInf_mono fun _ => le_iInf fun _ => le_rfl
Inclusion of Cofilters: $\text{coLindelof}\, X \leq \text{coclosedLindelof}\, X$
Informal description
For any topological space $X$, the cofilter of Lindelöf sets is finer than the filter of complements of closed Lindelöf sets. In other words, every set in the filter of complements of closed Lindelöf sets is also in the cofilter of Lindelöf sets.
IsLindeof.compl_mem_coclosedLindelof_of_isClosed theorem
(hs : IsLindelof s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedLindelof X
Full source 
theorem IsLindeof.compl_mem_coclosedLindelof_of_isClosed (hs : IsLindelof s) (hs' : IsClosed s) :
    sᶜsᶜ ∈ Filter.coclosedLindelof X :=
  hasBasis_coclosedLindelof.mem_of_mem ⟨hs', hs⟩
Complement of Closed Lindelöf Set in Coclosed Lindelöf Filter
Informal description
For any subset $s$ of a topological space $X$, if $s$ is both Lindelöf and closed, then its complement $s^c$ belongs to the filter of complements of closed Lindelöf sets.
LindelofSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- X is a Lindelöf space iff every open cover has a countable subcover. -/
class LindelofSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a Lindelöf space, `Set.univ` is a Lindelöf set. -/
  isLindelof_univ : IsLindelof (univ : Set X)
Lindelöf space
Informal description
A topological space \( X \) is called a Lindelöf space if every open cover of \( X \) has a countable subcover.
isLindelof_univ theorem
[h : LindelofSpace X] : IsLindelof (univ : Set X)
Full source 
theorem isLindelof_univ [h : LindelofSpace X] : IsLindelof (univ : Set X) :=
  h.isLindelof_univ
Universal Set is Lindelöf in a Lindelöf Space
Informal description
If $X$ is a Lindelöf space, then the entire space $X$ (as a subset) is Lindelöf.
cluster_point_of_Lindelof theorem
[LindelofSpace X] (f : Filter X) [NeBot f] [CountableInterFilter f] : ∃ x, ClusterPt x f
Full source 
theorem cluster_point_of_Lindelof [LindelofSpace X] (f : Filter X) [NeBot f]
    [CountableInterFilter f] : ∃ x, ClusterPt x f := by
  simpa using isLindelof_univ (show f ≤ 𝓟 univ by simp)
Existence of Cluster Points for Non-Trivial Filters in Lindelöf Spaces
Informal description
In a Lindelöf space $X$, every non-trivial filter $f$ on $X$ with the countable intersection property has a cluster point. That is, there exists a point $x \in X$ such that $x$ is a cluster point of $f$.
LindelofSpace.elim_nhds_subcover theorem
[LindelofSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ
Full source 
theorem LindelofSpace.elim_nhds_subcover [LindelofSpace X] (U : X → Set X) (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ := by
  obtain ⟨t, tc, -, s⟩ := IsLindelof.elim_nhds_subcover isLindelof_univ U fun x _ => hU x
  use t, tc
  apply top_unique s
Existence of Countable Neighborhood Cover in Lindelöf Spaces
Informal description
Let $X$ be a Lindelöf space. For any function $U : X \to \text{Set } X$ such that $U(x)$ is a neighborhood of $x$ for every $x \in X$, there exists a countable subset $t \subseteq X$ such that the union $\bigcup_{x \in t} U(x)$ covers the entire space $X$.
lindelofSpace_of_countable_subfamily_closed theorem
(h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u : Set ι, u.Countable ∧ ⋂ i ∈ u, t i = ∅) : LindelofSpace X
Full source 
theorem lindelofSpace_of_countable_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ →
      ∃ u : Set ι, u.Countable ∧ ⋂ i ∈ u, t i = ∅) :
    LindelofSpace X where
  isLindelof_univ := isLindelof_of_countable_subfamily_closed fun t => by simpa using h t
Lindelöf Property via Countable Intersections of Closed Sets
Informal description
A topological space $X$ is Lindelöf if for every family of closed sets $\{t_i\}_{i \in \iota}$ in $X$ with $\bigcap_{i} t_i = \emptyset$, there exists a countable subset $\iota' \subseteq \iota$ such that $\bigcap_{i \in \iota'} t_i = \emptyset$.
IsCompact.isLindelof theorem
(hs : IsCompact s) : IsLindelof s
Full source 
/-- A compact set `s` is Lindelöf. -/
theorem IsCompact.isLindelof (hs : IsCompact s) :
    IsLindelof s := by tauto
Compact sets are Lindelöf
Informal description
If a subset $s$ of a topological space $X$ is compact, then it is Lindelöf.
IsSigmaCompact.isLindelof theorem
(hs : IsSigmaCompact s) : IsLindelof s
Full source 
/-- A σ-compact set `s` is Lindelöf -/
theorem IsSigmaCompact.isLindelof (hs : IsSigmaCompact s) :
    IsLindelof s := by
  rw [IsSigmaCompact] at hs
  rcases hs with ⟨K, ⟨hc, huniv⟩⟩
  rw [← huniv]
  have hl : ∀ n, IsLindelof (K n) := fun n ↦ IsCompact.isLindelof (hc n)
  exact isLindelof_iUnion hl
$\sigma$-Compact Sets are Lindelöf
Informal description
If a subset $s$ of a topological space $X$ is $\sigma$-compact, then $s$ is Lindelöf.
instLindelofSpaceOfCompactSpace instance
[CompactSpace X] : LindelofSpace X
Full source 
/-- A compact space `X` is Lindelöf. -/
instance (priority := 100) [CompactSpace X] : LindelofSpace X :=
  { isLindelof_univ := isCompact_univ.isLindelof}
Compact Spaces are Lindelöf
Informal description
Every compact topological space $X$ is a Lindelöf space.
instLindelofSpaceOfSigmaCompactSpace instance
[SigmaCompactSpace X] : LindelofSpace X
Full source 
/-- A sigma-compact space `X` is Lindelöf. -/
instance (priority := 100) [SigmaCompactSpace X] : LindelofSpace X :=
  { isLindelof_univ := isSigmaCompact_univ.isLindelof}
$\sigma$-Compact Spaces are Lindelöf
Informal description
Every $\sigma$-compact topological space $X$ is a Lindelöf space.
NonLindelofSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- `X` is a non-Lindelöf topological space if it is not a Lindelöf space. -/
class NonLindelofSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a non-Lindelöf space, `Set.univ` is not a Lindelöf set. -/
  nonLindelof_univ : ¬IsLindelof (univ : Set X)
Non-Lindelöf space
Informal description
A topological space \( X \) is called a non-Lindelöf space if it is not a Lindelöf space, meaning there exists at least one open cover of \( X \) that does not admit a countable subcover.
IsLindelof.ne_univ theorem
[NonLindelofSpace X] (hs : IsLindelof s) : s ≠ univ
Full source 
theorem IsLindelof.ne_univ [NonLindelofSpace X] (hs : IsLindelof s) : s ≠ univ := fun h ↦
  nonLindelof_univ X (h ▸ hs)
Lindelöf subsets of non-Lindelöf spaces are proper subsets
Informal description
If $X$ is a non-Lindelöf space and $s$ is a Lindelöf subset of $X$, then $s$ is not equal to the universal set $X$.
instNeBotCoLindelofOfNonLindelofSpace instance
[NonLindelofSpace X] : NeBot (Filter.coLindelof X)
Full source 
instance [NonLindelofSpace X] : NeBot (Filter.coLindelof X) := by
  refine hasBasis_coLindelof.neBot_iff.2 fun {s} hs => ?_
  contrapose hs
  rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs
  rw [hs]
  exact nonLindelof_univ X
Non-triviality of the Co-Lindelöf Filter in Non-Lindelöf Spaces
Informal description
For any non-Lindelöf space $X$, the co-Lindelöf filter on $X$ is non-trivial (i.e., it does not contain the empty set).
instNeBotCoclosedLindelofOfNonLindelofSpace instance
[NonLindelofSpace X] : NeBot (Filter.coclosedLindelof X)
Full source 
instance [NonLindelofSpace X] : NeBot (Filter.coclosedLindelof X) :=
  neBot_of_le coLindelof_le_coclosedLindelof
Non-triviality of the Coclosed Lindelöf Filter in Non-Lindelöf Spaces
Informal description
For any non-Lindelöf space $X$, the filter of complements of closed Lindelöf sets on $X$ is non-trivial (i.e., it does not contain the empty set).
nonLindelofSpace_of_neBot theorem
(_ : NeBot (Filter.coLindelof X)) : NonLindelofSpace X
Full source 
theorem nonLindelofSpace_of_neBot (_ : NeBot (Filter.coLindelof X)) : NonLindelofSpace X :=
  ⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_coLindelof).ne_empty compl_univ⟩
Non-trivial co-Lindelöf filter implies non-Lindelöf space
Informal description
If the co-Lindelöf filter on a topological space $X$ is non-trivial (i.e., `NeBot (Filter.coLindelof X)` holds), then $X$ is a non-Lindelöf space.
instLindelofSpaceOfCompactSpace_1 instance
[CompactSpace X] : LindelofSpace X
Full source 
/-- A compact space `X` is Lindelöf. -/
instance (priority := 100) [CompactSpace X] : LindelofSpace X :=
  { isLindelof_univ := isCompact_univ.isLindelof}
Compact Spaces are Lindelöf
Informal description
Every compact topological space $X$ is a Lindelöf space.
countable_cover_nhds_interior theorem
[LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, interior (U x) = univ
Full source 
theorem countable_cover_nhds_interior [LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, interior (U x) = univ :=
  let ⟨t, ht⟩ := isLindelof_univ.elim_countable_subcover (fun x => interior (U x))
    (fun _ => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
  ⟨t, ⟨ht.1, univ_subset_iff.1 ht.2⟩⟩
Existence of Countable Interior Cover in Lindelöf Spaces
Informal description
Let $X$ be a Lindelöf space and $\{U(x)\}_{x \in X}$ be a family of neighborhoods of each point $x \in X$ (i.e., $U(x)$ is a neighborhood of $x$ for every $x \in X$). Then there exists a countable subset $t \subseteq X$ such that the union of the interiors of $U(x)$ for $x \in t$ covers $X$, i.e., $\bigcup_{x \in t} \text{interior}(U(x)) = X$.
countable_cover_nhds theorem
[LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) : ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ
Full source 
theorem countable_cover_nhds [LindelofSpace X] {U : X → Set X} (hU : ∀ x, U x ∈ 𝓝 x) :
    ∃ t : Set X, t.Countable ∧ ⋃ x ∈ t, U x = univ :=
  let ⟨t, ht⟩ := countable_cover_nhds_interior hU
  ⟨t, ⟨ht.1, univ_subset_iff.1 <| ht.2.symm.subset.trans <|
    iUnion₂_mono fun _ _ => interior_subset⟩⟩
Existence of Countable Neighborhood Cover in Lindelöf Spaces
Informal description
Let $X$ be a Lindelöf space and $\{U(x)\}_{x \in X}$ be a family of neighborhoods of each point $x \in X$ (i.e., $U(x)$ is a neighborhood of $x$ for every $x \in X$). Then there exists a countable subset $t \subseteq X$ such that the union of $U(x)$ for $x \in t$ covers $X$, i.e., $\bigcup_{x \in t} U(x) = X$.
Filter.comap_coLindelof_le theorem
{f : X → Y} (hf : Continuous f) : (Filter.coLindelof Y).comap f ≤ Filter.coLindelof X
Full source 
/-- 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 Filter.comap_coLindelof_le {f : X → Y} (hf : Continuous f) :
    (Filter.coLindelof Y).comap f ≤ Filter.coLindelof X := by
  rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]
  intro t ht
  refine ⟨f '' t, ht.image hf, ?_⟩
  simpa using t.subset_preimage_image f
Preimage of Co-Lindelöf Filter under Continuous Map is Coarser than Co-Lindelöf Filter
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ a continuous function. Then the preimage of the co-Lindelöf filter on $Y$ under $f$ is contained in the co-Lindelöf filter on $X$. In other words, for any subset $s \subseteq Y$ whose complement is Lindelöf, the preimage $f^{-1}(s)$ has a Lindelöf complement in $X$.
isLindelof_range theorem
[LindelofSpace X] {f : X → Y} (hf : Continuous f) : IsLindelof (range f)
Full source 
theorem isLindelof_range [LindelofSpace X] {f : X → Y} (hf : Continuous f) :
    IsLindelof (range f) := by rw [← image_univ]; exact isLindelof_univ.image hf
Continuous Image of a Lindelöf Space is Lindelöf
Informal description
Let $X$ be a Lindelöf space and $Y$ a topological space. For any continuous function $f \colon X \to Y$, the range of $f$ is a Lindelöf subset of $Y$.
Topology.IsInducing.isLindelof_iff theorem
{f : X → Y} (hf : IsInducing f) : IsLindelof s ↔ IsLindelof (f '' s)
Full source 
/-- 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 Topology.IsInducing.isLindelof_iff {f : X → Y} (hf : IsInducing f) :
    IsLindelofIsLindelof s ↔ IsLindelof (f '' s) := by
  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩
Lindelöf Property Preservation under Inducing Maps
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ an inducing map. Then $s$ is Lindelöf if and only if its image $f(s)$ is Lindelöf in $Y$.
Topology.IsEmbedding.isLindelof_iff theorem
{f : X → Y} (hf : IsEmbedding f) : IsLindelof s ↔ IsLindelof (f '' s)
Full source 
/-- 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 Topology.IsEmbedding.isLindelof_iff {f : X → Y} (hf : IsEmbedding f) :
    IsLindelofIsLindelof s ↔ IsLindelof (f '' s) := hf.isInducing.isLindelof_iff
Lindelöf Property Preservation under Embeddings
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a subset, and $f \colon X \to Y$ an embedding. Then $s$ is Lindelöf if and only if its image $f(s)$ is Lindelöf in $Y$.
Topology.IsInducing.isLindelof_preimage theorem
{f : X → Y} (hf : IsInducing f) (hf' : IsClosed (range f)) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K)
Full source 
/-- The preimage of a Lindelöf set under an inducing map is a Lindelöf set. -/
theorem Topology.IsInducing.isLindelof_preimage {f : X → Y} (hf : IsInducing f)
    (hf' : IsClosed (range f)) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K) := by
  replace hK := hK.inter_right hf'
  rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]
Preimage of Lindelöf Set under Inducing Map with Closed Range is Lindelöf
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ an inducing map with closed range, and $K \subseteq Y$ a Lindelöf set. Then the preimage $f^{-1}(K)$ is a Lindelöf set in $X$.
Topology.IsClosedEmbedding.isLindelof_preimage theorem
{f : X → Y} (hf : IsClosedEmbedding f) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K)
Full source 
/-- The preimage of a Lindelöf set under a closed embedding is a Lindelöf set. -/
theorem Topology.IsClosedEmbedding.isLindelof_preimage {f : X → Y} (hf : IsClosedEmbedding f)
    {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K) :=
  hf.isInducing.isLindelof_preimage (hf.isClosed_range) hK
Preimage of Lindelöf Set under Closed Embedding is Lindelöf
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a closed embedding, and $K \subseteq Y$ a Lindelöf set. Then the preimage $f^{-1}(K)$ is a Lindelöf set in $X$.
Topology.IsClosedEmbedding.tendsto_coLindelof theorem
{f : X → Y} (hf : IsClosedEmbedding f) : Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y)
Full source 
/-- 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
`Topology.IsClosedEmbedding.isLindelof_preimage`. -/
theorem Topology.IsClosedEmbedding.tendsto_coLindelof {f : X → Y} (hf : IsClosedEmbedding f) :
    Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y) :=
  hasBasis_coLindelof.tendsto_right_iff.mpr fun _K hK =>
    (hf.isLindelof_preimage hK).compl_mem_coLindelof
Closed Embeddings Preserve the Co-Lindelöf Filter
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ a closed embedding. Then $f$ maps the co-Lindelöf filter on $X$ to the co-Lindelöf filter on $Y$, i.e., for any set $s$ in the co-Lindelöf filter of $X$, its image $f(s)$ is in the co-Lindelöf filter of $Y$.
Subtype.isLindelof_iff theorem
{p : X → Prop} {s : Set { x // p x }} : IsLindelof s ↔ IsLindelof ((↑) '' s : Set X)
Full source 
/-- Sets of subtype are Lindelöf iff the image under a coercion is. -/
theorem Subtype.isLindelof_iff {p : X → Prop} {s : Set { x // p x }} :
    IsLindelofIsLindelof s ↔ IsLindelof ((↑) '' s : Set X) :=
  IsEmbedding.subtypeVal.isLindelof_iff
Lindelöf Property of Subtype via Canonical Inclusion
Informal description
Let $X$ be a topological space and $p \colon X \to \text{Prop}$ a predicate on $X$. For any subset $s$ of the subtype $\{x \in X \mid p(x)\}$, $s$ is Lindelöf if and only if its image under the canonical inclusion map $\uparrow \colon \{x \in X \mid p(x)\} \to X$ is Lindelöf in $X$.
Topology.IsClosedEmbedding.nonLindelofSpace theorem
[NonLindelofSpace X] {f : X → Y} (hf : IsClosedEmbedding f) : NonLindelofSpace Y
Full source 
protected theorem Topology.IsClosedEmbedding.nonLindelofSpace [NonLindelofSpace X] {f : X → Y}
    (hf : IsClosedEmbedding f) : NonLindelofSpace Y :=
  nonLindelofSpace_of_neBot hf.tendsto_coLindelof.neBot
Non-Lindelöf Property Preserved under Closed Embeddings
Informal description
Let $X$ be a non-Lindelöf space and $f \colon X \to Y$ a closed embedding. Then $Y$ is also a non-Lindelöf space.
Topology.IsClosedEmbedding.LindelofSpace theorem
[h : LindelofSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) : LindelofSpace X
Full source 
protected theorem Topology.IsClosedEmbedding.LindelofSpace [h : LindelofSpace Y] {f : X → Y}
    (hf : IsClosedEmbedding f) : LindelofSpace X :=
  ⟨by rw [hf.isInducing.isLindelof_iff, image_univ]; exact hf.isClosed_range.isLindelof⟩
Lindelöf Property Preserved under Closed Embeddings
Informal description
Let $Y$ be a Lindelöf space and $f \colon X \to Y$ be a closed embedding. Then $X$ is also a Lindelöf space.
Countable.LindelofSpace instance
[Countable X] : LindelofSpace X
Full source 
/-- Countable topological spaces are Lindelof. -/
instance (priority := 100) Countable.LindelofSpace [Countable X] : LindelofSpace X where
  isLindelof_univ := countable_univ.isLindelof
Countable Spaces are Lindelöf
Informal description
Every countable topological space is a Lindelöf space.
instLindelofSpaceSum instance
[LindelofSpace X] [LindelofSpace Y] : LindelofSpace (X ⊕ Y)
Full source 
/-- The disjoint union of two Lindelöf spaces is Lindelöf. -/
instance [LindelofSpace X] [LindelofSpace Y] : LindelofSpace (X ⊕ Y) where
  isLindelof_univ := by
    rw [← range_inl_union_range_inr]
    exact (isLindelof_range continuous_inl).union (isLindelof_range continuous_inr)
Disjoint Union of Lindelöf Spaces is Lindelöf
Informal description
For any two Lindelöf spaces $X$ and $Y$, their disjoint union $X \sqcup Y$ is also a Lindelöf space.
instLindelofSpaceSigmaOfCountable instance
{X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)] [∀ i, LindelofSpace (X i)] : LindelofSpace (Σ i, X i)
Full source 
instance {X : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (X i)] [∀ i, LindelofSpace (X i)] :
    LindelofSpace (Σi, X i) where
  isLindelof_univ := by
    rw [Sigma.univ]
    exact isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk
Countable Disjoint Union of Lindelöf Spaces is Lindelöf
Informal description
For any countable index type $\iota$ and a family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a Lindelöf space, the disjoint union $\Sigma i, X_i$ is also a Lindelöf space.
Quot.LindelofSpace instance
{r : X → X → Prop} [LindelofSpace X] : LindelofSpace (Quot r)
Full source 
instance Quot.LindelofSpace {r : X → X → Prop} [LindelofSpace X] : LindelofSpace (Quot r) where
  isLindelof_univ := by
    rw [← range_quot_mk]
    exact isLindelof_range continuous_quot_mk
Lindelöf Property Preserved under Quotient Construction
Informal description
For any topological space $X$ that is Lindelöf and any equivalence relation $r$ on $X$, the quotient space $\mathrm{Quot}\, r$ is also Lindelöf.
Quotient.LindelofSpace instance
{s : Setoid X} [LindelofSpace X] : LindelofSpace (Quotient s)
Full source 
instance Quotient.LindelofSpace {s : Setoid X} [LindelofSpace X] : LindelofSpace (Quotient s) :=
  Quot.LindelofSpace
Lindelöf Property Preserved under Quotient by Setoid
Informal description
For any topological space $X$ that is Lindelöf and any setoid $s$ on $X$, the quotient space $\mathrm{Quotient}\, s$ is also Lindelöf.
LindelofSpace.of_continuous_surjective theorem
{f : X → Y} [LindelofSpace X] (hf : Continuous f) (hsur : Function.Surjective f) : LindelofSpace Y
Full source 
/-- A continuous image of a Lindelöf set is a Lindelöf set within the codomain. -/
theorem LindelofSpace.of_continuous_surjective {f : X → Y} [LindelofSpace X] (hf : Continuous f)
    (hsur : Function.Surjective f) : LindelofSpace Y where
  isLindelof_univ := by
    rw [← Set.image_univ_of_surjective hsur]
    exact IsLindelof.image (isLindelof_univ_iff.mpr ‹_›) hf
Continuous Surjective Image of a Lindelöf Space is Lindelöf
Informal description
Let $X$ and $Y$ be topological spaces, with $X$ being Lindelöf. If $f \colon X \to Y$ is a continuous surjective map, then $Y$ is also a Lindelöf space.
IsHereditarilyLindelof definition
(s : Set X)
Full source 
/-- 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. -/
def IsHereditarilyLindelof (s : Set X) :=
  ∀ t ⊆ s, IsLindelof t
Hereditarily Lindelöf set
Informal description
A subset $s$ of a topological space $X$ is called hereditarily Lindelöf if every subset $t$ of $s$ is a Lindelöf set, where a Lindelöf set is one where every open cover has a countable subcover.
HereditarilyLindelofSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- Type class for Hereditarily Lindelöf spaces. -/
class HereditarilyLindelofSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a Hereditarily Lindelöf space, `Set.univ` is a Hereditarily Lindelöf set. -/
  isHereditarilyLindelof_univ : IsHereditarilyLindelof (univ : Set X)
Hereditarily Lindelöf space
Informal description
A topological space $X$ is called hereditarily Lindelöf if every subset of $X$ is Lindelöf, where a subset $s$ is Lindelöf if every open cover of $s$ has a countable subcover.
IsHereditarilyLindelof.isLindelof_subset theorem
(hs : IsHereditarilyLindelof s) (ht : t ⊆ s) : IsLindelof t
Full source 
lemma IsHereditarilyLindelof.isLindelof_subset (hs : IsHereditarilyLindelof s) (ht : t ⊆ s) :
    IsLindelof t := hs t ht
Subsets of Hereditarily Lindelöf Sets are Lindelöf
Informal description
If a subset $s$ of a topological space $X$ is hereditarily Lindelöf and $t$ is a subset of $s$, then $t$ is Lindelöf.
HereditarilyLindelof_LindelofSets theorem
[HereditarilyLindelofSpace X] (s : Set X) : IsLindelof s
Full source 
theorem HereditarilyLindelof_LindelofSets [HereditarilyLindelofSpace X] (s : Set X) :
    IsLindelof s := by
  apply HereditarilyLindelofSpace.isHereditarilyLindelof_univ
  exact subset_univ s
Subsets of Hereditarily Lindelöf Spaces are Lindelöf
Informal description
For a hereditarily Lindelöf topological space $X$, every subset $s \subseteq X$ is a Lindelöf set. That is, every open cover of $s$ has a countable subcover.
SecondCountableTopology.toHereditarilyLindelof instance
[SecondCountableTopology X] : HereditarilyLindelofSpace X
Full source 
instance (priority := 100) SecondCountableTopology.toHereditarilyLindelof
    [SecondCountableTopology X] : HereditarilyLindelofSpace X where
  isHereditarilyLindelof_univ t _ _ := by
    apply isLindelof_iff_countable_subcover.mpr
    intro ι U hι hcover
    have := @isOpen_iUnion_countable X _ _ ι U hι
    rcases this with ⟨t, ⟨htc, htu⟩⟩
    use t, htc
    exact subset_of_subset_of_eq hcover (id htu.symm)
Second-Countable Spaces are Hereditarily Lindelöf
Informal description
Every second-countable topological space $X$ is hereditarily Lindelöf.
HereditarilyLindelof.lindelofSpace_subtype instance
[HereditarilyLindelofSpace X] (p : X → Prop) : LindelofSpace { x // p x }
Full source 
instance HereditarilyLindelof.lindelofSpace_subtype [HereditarilyLindelofSpace X] (p : X → Prop) :
    LindelofSpace {x // p x} := by
  apply isLindelof_iff_LindelofSpace.mp
  exact HereditarilyLindelof_LindelofSets fun x ↦ p x
Subspaces of Hereditarily Lindelöf Spaces are Lindelöf
Informal description
For any hereditarily Lindelöf topological space $X$ and any predicate $p$ on $X$, the subspace $\{x \in X \mid p(x)\}$ is a Lindelöf space.