Mathlib.Topology.Bases

TopologicalSpace.IsTopologicalBasis structure

(s : Set (Set α))

Full source

/-- A topological basis is one that satisfies the necessary conditions so that
  it suffices to take unions of the basis sets to get a topology (without taking
  finite intersections as well). -/
structure IsTopologicalBasis (s : Set (Set α)) : Prop where
  /-- For every point `x`, the set of `t ∈ s` such that `x ∈ t` is directed downwards. -/
  exists_subset_inter : ∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
  /-- The sets from `s` cover the whole space. -/
  sUnion_eq : ⋃₀ s = univ
  /-- The topology is generated by sets from `s`. -/
  eq_generateFrom : t = generateFrom s

Topological Basis

Informal description

A collection of sets $ s $ in a topological space $ \alpha $ is called a *topological basis* if every open set in the space can be expressed as a union of sets from $ s $, without the need to take finite intersections of these sets.

TopologicalSpace.isTopologicalBasis_of_subbasis theorem

 {s : Set (Set α)} (hs : t = generateFrom s) :
  IsTopologicalBasis ((fun f => ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ s})

Full source

/-- If a family of sets `s` generates the topology, then intersections of finite
subcollections of `s` form a topological basis. -/
theorem isTopologicalBasis_of_subbasis {s : Set (Set α)} (hs : t = generateFrom s) :
    IsTopologicalBasis ((fun f => ⋂₀ f) '' { f : Set (Set α) | f.Finite ∧ f ⊆ s }) := by
  subst t; letI := generateFrom s
  refine ⟨?_, ?_, le_antisymm (le_generateFrom ?_) <| generateFrom_anti fun t ht => ?_⟩
  · rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
    exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
  · rw [sUnion_image, iUnion₂_eq_univ_iff]
    exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
  · rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
    exact hft.isOpen_sInter fun s hs ↦ GenerateOpen.basic _ <| htb hs
  · rw [← sInter_singleton t]
    exact ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩

Finite Intersections of Subbasis Form a Topological Basis

Informal description

Let $t$ be a topological space on a type $\alpha$ generated by a collection of sets $s$ (i.e., $t = \text{generateFrom } s$). Then the collection of all finite intersections of sets from $s$ forms a topological basis for $t$.

TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInter theorem

{s : Set (Set α)} (hsg : t = generateFrom s) (hsi : FiniteInter s) : IsTopologicalBasis s

Full source

theorem isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s)
    (hsi : FiniteInter s) : IsTopologicalBasis s := by
  convert isTopologicalBasis_of_subbasis hsg
  refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_
  rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩
  lift g to Finset (Set α) using hg
  exact hsi.finiteInter_mem g hgs

Finite Intersection Property Implies Basis for Generated Topology

Informal description

Let $s$ be a collection of subsets of a topological space $\alpha$ such that: 1. The topology $t$ on $\alpha$ is generated by $s$ (i.e., $t = \text{generateFrom } s$), and 2. $s$ is closed under finite intersections (i.e., $s$ has the `FiniteInter` property). Then $s$ forms a topological basis for the space $\alpha$.

TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter theorem

 {r : Set (Set α)} (hsg : t = generateFrom r) (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ t ∈ r) :
  IsTopologicalBasis (insert univ r)

Full source

theorem isTopologicalBasis_of_subbasis_of_inter {r : Set (Set α)} (hsg : t = generateFrom r)
    (hsi : ∀ ⦃s⦄, s ∈ r → ∀ ⦃t⦄, t ∈ r → s ∩ ts ∩ t ∈ r) : IsTopologicalBasis (insert univ r) :=
  isTopologicalBasis_of_subbasis_of_finiteInter (by simpa using hsg) (FiniteInter.mk₂ hsi)

Universal Set Extension of Intersection-Closed Subbasis Forms a Topological Basis

Informal description

Let $X$ be a topological space with topology $t$ generated by a collection of subsets $r$ (i.e., $t = \text{generateFrom } r$). If $r$ is closed under finite intersections (i.e., for any $s, t \in r$, their intersection $s \cap t$ is also in $r$), then the collection obtained by adding the universal set to $r$ forms a topological basis for $X$.

TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds theorem

{s : Set (Set α)} (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s

Full source

theorem IsTopologicalBasis.of_hasBasis_nhds {s : Set (Set α)}
    (h_nhds : ∀ a, (𝓝 a).HasBasis (fun t ↦ t ∈ st ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s where
  exists_subset_inter t₁ ht₁ t₂ ht₂ x hx := by
    simpa only [and_assoc, (h_nhds x).mem_iff]
      using (inter_mem ((h_nhds _).mem_of_mem ⟨ht₁, hx.1⟩) ((h_nhds _).mem_of_mem ⟨ht₂, hx.2⟩))
  sUnion_eq := sUnion_eq_univ_iff.2 fun x ↦ (h_nhds x).ex_mem
  eq_generateFrom := ext_nhds fun x ↦ by
    simpa only [nhds_generateFrom, and_comm] using (h_nhds x).eq_biInf

Topological Basis Characterization via Neighborhood Basis

Informal description

Let $X$ be a topological space and $s$ be a collection of subsets of $X$. Suppose that for every point $a \in X$, the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of sets in $s$ that contain $a$ (i.e., $\mathcal{N}(a)$ is generated by $\{ t \in s \mid a \in t \}$). Then $s$ is a topological basis for $X$.

TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds theorem

 {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)
  (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : IsTopologicalBasis s

Full source

/-- If a family of open sets `s` is such that every open neighbourhood contains some
member of `s`, then `s` is a topological basis. -/
theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u)
    (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) :
    IsTopologicalBasis s :=
  .of_hasBasis_nhds <| fun a ↦
    (nhds_basis_opens a).to_hasBasis' (by simpa [and_assoc] using h_nhds a)
      fun _ ⟨hts, hat⟩ ↦ (h_open _ hts).mem_nhds hat

Characterization of Topological Basis via Open Neighborhoods

Informal description

Let $X$ be a topological space and $s$ be a collection of open subsets of $X$. Suppose that for every point $a \in X$ and every open neighborhood $u$ of $a$, there exists a set $v \in s$ such that $a \in v$ and $v \subseteq u$. Then $s$ is a topological basis for $X$.

TopologicalSpace.IsTopologicalBasis.mem_nhds_iff theorem

 {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Full source

/-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which
contains `a` and is itself contained in `s`. -/
theorem IsTopologicalBasis.mem_nhds_iff {a : α} {s : Set α} {b : Set (Set α)}
    (hb : IsTopologicalBasis b) : s ∈ 𝓝 as ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s := by
  change s ∈ (𝓝 a).setss ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
  rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
  · simp [and_assoc, and_left_comm]
  · rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
    let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
    exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩
  · rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
    exact ⟨i, h2, h1⟩

Neighborhood Characterization via Topological Basis

Informal description

Let $b$ be a topological basis for a topological space $\alpha$, and let $a \in \alpha$ and $s \subseteq \alpha$. Then $s$ is a neighborhood of $a$ if and only if there exists a basis set $t \in b$ such that $a \in t$ and $t \subseteq s$.

TopologicalSpace.IsTopologicalBasis.isOpen_iff theorem

 {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Full source

theorem IsTopologicalBasis.isOpen_iff {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) :
    IsOpenIsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s := by simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

Characterization of Open Sets via Topological Basis

Informal description

Let $b$ be a topological basis for a topological space $\alpha$. A subset $s \subseteq \alpha$ is open if and only if for every point $a \in s$, there exists a basis set $t \in b$ such that $a \in t$ and $t \subseteq s$.

TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset theorem

 {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : IsTopologicalBasis s) (hss' : s ⊆ s') : IsTopologicalBasis s'

Full source

theorem IsTopologicalBasis.of_isOpen_of_subset {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u)
    (hs : IsTopologicalBasis s) (hss' : s ⊆ s') : IsTopologicalBasis s' :=
  isTopologicalBasis_of_isOpen_of_nhds h_open fun a _ ha u_open ↦
    have ⟨t, hts, ht⟩ := hs.isOpen_iff.mp u_open a ha; ⟨t, hss' hts, ht⟩

Extension of Topological Basis by Open Superset

Informal description

Let $s$ and $s'$ be collections of subsets of a topological space $\alpha$ such that: 1. Every set in $s'$ is open, 2. $s$ is a topological basis for $\alpha$, and 3. $s$ is a subset of $s'$. Then $s'$ is also a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.nhds_hasBasis theorem

 {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} : (𝓝 a).HasBasis (fun t : Set α => t ∈ b ∧ a ∈ t) fun t => t

Full source

theorem IsTopologicalBasis.nhds_hasBasis {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} :
    (𝓝 a).HasBasis (fun t : Set α => t ∈ bt ∈ b ∧ a ∈ t) fun t => t :=
  ⟨fun s => hb.mem_nhds_iff.trans <| by simp only [and_assoc]⟩

Neighborhood Filter Basis Characterization via Topological Basis

Informal description

Let $b$ be a topological basis for a topological space $\alpha$ and let $a \in \alpha$. Then the neighborhood filter $\mathcal{N}(a)$ has a basis consisting of those sets $t \in b$ that contain $a$, i.e., $\mathcal{N}(a)$ is generated by $\{t \in b \mid a \in t\}$.

TopologicalSpace.IsTopologicalBasis.isOpen theorem

{s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s

Full source

protected theorem IsTopologicalBasis.isOpen {s : Set α} {b : Set (Set α)}
    (hb : IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s := by
  rw [hb.eq_generateFrom]
  exact .basic s hs

Openness of Basis Sets in a Topological Basis

Informal description

Let $b$ be a topological basis for a topological space $\alpha$. For any set $s \in b$, $s$ is open in $\alpha$.

TopologicalSpace.IsTopologicalBasis.insert_empty theorem

{s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (insert ∅ s)

Full source

theorem IsTopologicalBasis.insert_empty {s : Set (Set α)} (h : IsTopologicalBasis s) :
    IsTopologicalBasis (insert ∅ s) :=
  h.of_isOpen_of_subset (by rintro _ (rfl | hu); exacts [isOpen_empty, h.isOpen hu])
    (subset_insert ..)

Insertion of Empty Set Preserves Topological Basis Property

Informal description

Let $s$ be a topological basis for a topological space $\alpha$. Then the collection obtained by inserting the empty set into $s$, denoted $\{\emptyset\} \cup s$, is also a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.diff_empty theorem

{s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (s \ {∅})

Full source

theorem IsTopologicalBasis.diff_empty {s : Set (Set α)} (h : IsTopologicalBasis s) :
    IsTopologicalBasis (s \ {∅}) :=
  isTopologicalBasis_of_isOpen_of_nhds (fun _ hu ↦ h.isOpen hu.1) fun a _ ha hu ↦
    have ⟨t, hts, ht⟩ := h.isOpen_iff.mp hu a ha
    ⟨t, ⟨hts, ne_of_mem_of_not_mem' ht.1 <| not_mem_empty _⟩, ht⟩

Removing Empty Set Preserves Topological Basis Property

Informal description

Let $s$ be a topological basis for a topological space $\alpha$. Then the collection obtained by removing the empty set from $s$, denoted $s \setminus \{\emptyset\}$, is also a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.mem_nhds theorem

{a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ 𝓝 a

Full source

protected theorem IsTopologicalBasis.mem_nhds {a : α} {s : Set α} {b : Set (Set α)}
    (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ 𝓝 a :=
  (hb.isOpen hs).mem_nhds ha

Basis Sets are Neighborhoods of Their Points

Informal description

Let $b$ be a topological basis for a topological space $\alpha$. For any set $s \in b$ and any point $a \in s$, the set $s$ is a neighborhood of $a$ (i.e., $s \in \mathcal{N}(a)$).

TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open theorem

 {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u

Full source

theorem IsTopologicalBasis.exists_subset_of_mem_open {b : Set (Set α)} (hb : IsTopologicalBasis b)
    {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u :=
  hb.mem_nhds_iff.1 <| IsOpen.mem_nhds ou au

Existence of Basis Subset for Open Neighborhoods

Informal description

Let $b$ be a topological basis for a topological space $\alpha$. For any point $a \in \alpha$ and any open set $u \subseteq \alpha$ containing $a$, there exists a basis set $v \in b$ such that $a \in v$ and $v \subseteq u$.

TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' theorem

{B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : u = ⋃₀ {s ∈ B | s ⊆ u}

Full source

/-- Any open set is the union of the basis sets contained in it. -/
theorem IsTopologicalBasis.open_eq_sUnion' {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}
    (ou : IsOpen u) : u = ⋃₀ { s ∈ B | s ⊆ u } :=
  ext fun _a =>
    ⟨fun ha =>
      let ⟨b, hb, ab, bu⟩ := hB.exists_subset_of_mem_open ha ou
      ⟨b, ⟨hb, bu⟩, ab⟩,
      fun ⟨_b, ⟨_, bu⟩, ab⟩ => bu ab⟩

Open Sets as Unions of Basis Subsets

Informal description

Let $B$ be a topological basis for a topological space $\alpha$. For any open set $u \subseteq \alpha$, $u$ is equal to the union of all basis sets in $B$ that are contained in $u$, i.e., $$ u = \bigcup \{s \in B \mid s \subseteq u\}. $$

TopologicalSpace.IsTopologicalBasis.open_eq_sUnion theorem

{B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S

Full source

theorem IsTopologicalBasis.open_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}
    (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S :=
  ⟨{ s ∈ B | s ⊆ u }, fun _ h => h.1, hB.open_eq_sUnion' ou⟩

Open Sets as Unions of Basis Subsets (Existence Version)

Informal description

Let $B$ be a topological basis for a topological space $\alpha$. For any open set $u \subseteq \alpha$, there exists a subset $S \subseteq B$ such that $u$ is equal to the union of all sets in $S$, i.e., $u = \bigcup_{s \in S} s$.

TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion theorem

{B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S

Full source

theorem IsTopologicalBasis.open_iff_eq_sUnion {B : Set (Set α)} (hB : IsTopologicalBasis B)
    {u : Set α} : IsOpenIsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S :=
  ⟨hB.open_eq_sUnion, fun ⟨_S, hSB, hu⟩ => hu.symm ▸ isOpen_sUnion fun _s hs => hB.isOpen (hSB hs)⟩

Characterization of Open Sets via Basis Unions

Informal description

Let $B$ be a topological basis for a topological space $\alpha$. A subset $u \subseteq \alpha$ is open if and only if there exists a subset $S \subseteq B$ such that $u$ is equal to the union of all sets in $S$, i.e., $u = \bigcup_{s \in S} s$.

TopologicalSpace.IsTopologicalBasis.open_eq_iUnion theorem

 {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) :
  ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B

Full source

theorem IsTopologicalBasis.open_eq_iUnion {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α}
    (ou : IsOpen u) : ∃ (β : Type u) (f : β → Set α), (u = ⋃ i, f i) ∧ ∀ i, f i ∈ B :=
  ⟨↥({ s ∈ B | s ⊆ u }), (↑), by
    rw [← sUnion_eq_iUnion]
    apply hB.open_eq_sUnion' ou, fun s => And.left s.2⟩

Open Sets as Indexed Unions of Basis Elements

Informal description

Let $B$ be a topological basis for a topological space $\alpha$. For any open set $u \subseteq \alpha$, there exists an index type $\beta$ and a family of sets $f : \beta \to \text{Set } \alpha$ such that: 1. $u$ can be expressed as the union $\bigcup_{i \in \beta} f(i)$, and 2. each $f(i)$ belongs to the basis $B$.

TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset theorem

{t : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t

Full source

lemma IsTopologicalBasis.subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B)
    (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t := by
  rw [hB.open_eq_sUnion' hs]; simpa [sUnion_subset_iff]

Basis Sets Determine Open Subset Containment

Informal description

Let $B$ be a topological basis for a topological space $\alpha$, and let $s$ and $t$ be subsets of $\alpha$ such that $s$ is open. If every basis set $U \in B$ that is contained in $s$ is also contained in $t$, then $s$ is a subset of $t$.

TopologicalSpace.IsTopologicalBasis.mem_closure_iff theorem

 {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty

Full source

/-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`. -/
theorem IsTopologicalBasis.mem_closure_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α}
    {a : α} : a ∈ closure sa ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty :=
  (mem_closure_iff_nhds_basis' hb.nhds_hasBasis).trans <| by simp only [and_imp]

Closure Membership Criterion via Topological Basis

Informal description

Let $X$ be a topological space with a topological basis $b$, and let $s \subseteq X$ and $a \in X$. Then $a$ belongs to the closure of $s$ if and only if for every basis set $o \in b$ containing $a$, the intersection $o \cap s$ is nonempty.

TopologicalSpace.IsTopologicalBasis.dense_iff theorem

 {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} : Dense s ↔ ∀ o ∈ b, Set.Nonempty o → (o ∩ s).Nonempty

Full source

/-- A set is dense iff it has non-trivial intersection with all basis sets. -/
theorem IsTopologicalBasis.dense_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} :
    DenseDense s ↔ ∀ o ∈ b, Set.Nonempty o → (o ∩ s).Nonempty := by
  simp only [Dense, hb.mem_closure_iff]
  exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩

Density Criterion via Basis Sets

Informal description

Let $X$ be a topological space with a topological basis $b$. A subset $s \subseteq X$ is dense in $X$ if and only if for every nonempty basis set $o \in b$, the intersection $o \cap s$ is nonempty.

TopologicalSpace.IsTopologicalBasis.isOpenMap_iff theorem

 {β} [TopologicalSpace β] {B : Set (Set α)} (hB : IsTopologicalBasis B) {f : α → β} :
  IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)

Full source

theorem IsTopologicalBasis.isOpenMap_iff {β} [TopologicalSpace β] {B : Set (Set α)}
    (hB : IsTopologicalBasis B) {f : α → β} : IsOpenMapIsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s) := by
  refine ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => ?_⟩
  rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
  exact isOpen_iUnion fun s => hf s s.2.1

Open Map Characterization via Basis Sets

Informal description

Let $B$ be a topological basis for a topological space $\alpha$, and let $\beta$ be another topological space. A function $f : \alpha \to \beta$ is an open map if and only if for every basis set $s \in B$, the image $f(s)$ is open in $\beta$.

TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset theorem

 {B : Set (Set α)} (hb : IsTopologicalBasis B) {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) :
  ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u

Full source

theorem IsTopologicalBasis.exists_nonempty_subset {B : Set (Set α)} (hb : IsTopologicalBasis B)
    {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, Set.Nonempty v ∧ v ⊆ u :=
  let ⟨x, hx⟩ := hu
  let ⟨v, vB, xv, vu⟩ := hb.exists_subset_of_mem_open hx ou
  ⟨v, vB, ⟨x, xv⟩, vu⟩

Existence of Nonempty Basis Subset for Nonempty Open Sets

Informal description

Let $B$ be a topological basis for a topological space $\alpha$. For any nonempty open set $u \subseteq \alpha$, there exists a basis set $v \in B$ such that $v$ is nonempty and $v \subseteq u$.

TopologicalSpace.isTopologicalBasis_opens theorem

: IsTopologicalBasis {U : Set α | IsOpen U}

Full source

theorem isTopologicalBasis_opens : IsTopologicalBasis { U : Set α | IsOpen U } :=
  isTopologicalBasis_of_isOpen_of_nhds (by tauto) (by tauto)

Open Sets Form a Topological Basis

Informal description

The collection of all open sets in a topological space $\alpha$ forms a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.isInducing theorem

 {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)} (hf : IsInducing f) (h : IsTopologicalBasis T) :
  IsTopologicalBasis ((preimage f) '' T)

Full source

protected lemma IsTopologicalBasis.isInducing {β} [TopologicalSpace β] {f : α → β} {T : Set (Set β)}
    (hf : IsInducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis ((preimage f) '' T) :=
  .of_hasBasis_nhds fun a ↦ by
    convert (hf.basis_nhds (h.nhds_hasBasis (a := f a))).to_image_id with s
    aesop

Induced Topological Basis under Inducing Maps

Informal description

Let $f \colon \alpha \to \beta$ be an inducing map between topological spaces, and let $T$ be a topological basis for $\beta$. Then the collection of preimages $\{f^{-1}(U) \mid U \in T\}$ forms a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.induced theorem

 {α} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)} (h : IsTopologicalBasis T) :
  IsTopologicalBasis (t := induced f s) ((preimage f) '' T)

Full source

protected theorem IsTopologicalBasis.induced {α} [s : TopologicalSpace β] (f : α → β)
    {T : Set (Set β)} (h : IsTopologicalBasis T) :
    IsTopologicalBasis (t := induced f s) ((preimage f) '' T) :=
  h.isInducing (t := induced f s) (.induced f)

Induced Topological Basis from Preimages under a Function

Informal description

Let $\beta$ be a topological space with a topological basis $T$, and let $f : \alpha \to \beta$ be a function. Then the collection of preimages $\{f^{-1}(U) \mid U \in T\}$ forms a topological basis for the topology on $\alpha$ induced by $f$.

TopologicalSpace.IsTopologicalBasis.inf theorem

 {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)} (h₁ : IsTopologicalBasis (t := t₁) B₁)
  (h₂ : IsTopologicalBasis (t := t₂) B₂) : IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂)

Full source

protected theorem IsTopologicalBasis.inf {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)}
    (h₁ : IsTopologicalBasis (t := t₁) B₁) (h₂ : IsTopologicalBasis (t := t₂) B₂) :
    IsTopologicalBasis (t := t₁ ⊓ t₂) (image2 (· ∩ ·) B₁ B₂) := by
  refine .of_hasBasis_nhds (t := ?_) fun a ↦ ?_
  rw [nhds_inf (t₁ := t₁)]
  convert ((h₁.nhds_hasBasis (t := t₁)).inf (h₂.nhds_hasBasis (t := t₂))).to_image_id
  aesop

Intersection of Topological Bases Forms Basis for Infimum Topology

Informal description

Let $t₁$ and $t₂$ be two topologies on a type $\beta$, with topological bases $B₁$ and $B₂$ respectively. Then the collection of pairwise intersections $\{U \cap V \mid U \in B₁, V \in B₂\}$ forms a topological basis for the infimum topology $t₁ \sqcap t₂$.

TopologicalSpace.IsTopologicalBasis.inf_induced theorem

 {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁)
  (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α) (f₂ : γ → β) :
  IsTopologicalBasis (t := induced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂)

Full source

theorem IsTopologicalBasis.inf_induced {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)}
    {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α)
    (f₂ : γ → β) :
    IsTopologicalBasis (t := inducedinduced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' ·f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂) := by
  simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)

Topological Basis for Infimum of Induced Topologies via Preimages and Intersections

Informal description

Let $\alpha$ and $\beta$ be topological spaces with topological bases $B_1$ and $B_2$ respectively. Given functions $f_1 : \gamma \to \alpha$ and $f_2 : \gamma \to \beta$, the collection of sets of the form $f_1^{-1}(U) \cap f_2^{-1}(V)$ for $U \in B_1$ and $V \in B_2$ forms a topological basis for the infimum of the topologies on $\gamma$ induced by $f_1$ and $f_2$.

TopologicalSpace.IsTopologicalBasis.prod theorem

 {β} [TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁)
  (h₂ : IsTopologicalBasis B₂) : IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂)

Full source

protected theorem IsTopologicalBasis.prod {β} [TopologicalSpace β] {B₁ : Set (Set α)}
    {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) :
    IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) :=
  h₁.inf_induced h₂ Prod.fst Prod.snd

Product of Topological Bases Forms Basis for Product Topology

Informal description

Let $\alpha$ and $\beta$ be topological spaces with topological bases $B_1$ and $B_2$ respectively. Then the collection of Cartesian products $\{U \times V \mid U \in B_1, V \in B_2\}$ forms a topological basis for the product topology on $\alpha \times \beta$.

TopologicalSpace.isTopologicalBasis_of_cover theorem

 {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen (U i)) (Uc : ⋃ i, U i = univ) {b : ∀ i, Set (Set (U i))}
  (hb : ∀ i, IsTopologicalBasis (b i)) : IsTopologicalBasis (⋃ i : ι, image ((↑) : U i → α) '' b i)

Full source

theorem isTopologicalBasis_of_cover {ι} {U : ι → Set α} (Uo : ∀ i, IsOpen (U i))
    (Uc : ⋃ i, U i = univ) {b : ∀ i, Set (Set (U i))} (hb : ∀ i, IsTopologicalBasis (b i)) :
    IsTopologicalBasis (⋃ i : ι, image ((↑) : U i → α) '' b i) := by
  refine isTopologicalBasis_of_isOpen_of_nhds (fun u hu => ?_) ?_
  · simp only [mem_iUnion, mem_image] at hu
    rcases hu with ⟨i, s, sb, rfl⟩
    exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)
  · intro a u ha uo
    rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
    lift a to ↥(U i) using hi
    rcases (hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
      ⟨v, hvb, hav, hvu⟩
    exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩

Construction of Topological Basis from Open Cover and Subspace Bases

Informal description

Let $\{U_i\}_{i \in \iota}$ be an open cover of a topological space $\alpha$ (i.e., each $U_i$ is open and their union is the entire space). For each $i \in \iota$, let $b_i$ be a topological basis for the subspace topology on $U_i$. Then the collection of all images of the basis sets $b_i$ under the inclusion maps $U_i \hookrightarrow \alpha$ forms a topological basis for $\alpha$.

TopologicalSpace.IsTopologicalBasis.continuous_iff theorem

 {β : Type*} [TopologicalSpace β] {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :
  Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

Full source

protected theorem IsTopologicalBasis.continuous_iff {β : Type*} [TopologicalSpace β]
    {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} :
    ContinuousContinuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s) := by
  rw [hB.eq_generateFrom, continuous_generateFrom_iff]

Continuity Criterion via Basis: $f$ continuous iff preimages of basis elements are open

Informal description

Let $X$ and $Y$ be topological spaces, where $Y$ has a topological basis $B$. A function $f : X \to Y$ is continuous if and only if for every basic open set $s \in B$, the preimage $f^{-1}(s)$ is open in $X$.

TopologicalSpace.isTopologicalBasis_empty theorem

: IsTopologicalBasis (∅ : Set (Set α)) ↔ IsEmpty α

Full source

@[simp] lemma isTopologicalBasis_empty : IsTopologicalBasisIsTopologicalBasis (∅ : Set (Set α)) ↔ IsEmpty α where
  mp h := by simpa using h.sUnion_eq.symm
  mpr h := ⟨by simp, by simp [Set.univ_eq_empty_iff.2], Subsingleton.elim ..⟩

Empty Set as Topological Basis iff Space is Empty

Informal description

The empty collection of sets is a topological basis for a topological space $\alpha$ if and only if the space $\alpha$ is empty, i.e., $\emptyset$ is a topological basis for $\alpha$ $\leftrightarrow$ $\alpha$ is empty.

TopologicalSpace.SeparableSpace structure

Full source

/-- A separable space is one with a countable dense subset, available through
`TopologicalSpace.exists_countable_dense`. If `α` is also known to be nonempty, then
`TopologicalSpace.denseSeq` provides a sequence `ℕ → α` with dense range, see
`TopologicalSpace.denseRange_denseSeq`.

If `α` is a uniform space with countably generated uniformity filter (e.g., an `EMetricSpace`), then
this condition is equivalent to `SecondCountableTopology α`. In this case the
latter should be used as a typeclass argument in theorems because Lean can automatically deduce
`TopologicalSpace.SeparableSpace` from `SecondCountableTopology` but it can't
deduce `SecondCountableTopology` from `TopologicalSpace.SeparableSpace`.

Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: the previous paragraph describes the state of the art in Lean 3.
We can have instance cycles in Lean 4 but we might want to
postpone adding them till after the port. -/
@[mk_iff] class SeparableSpace : Prop where
  /-- There exists a countable dense set. -/
  exists_countable_dense : ∃ s : Set α, s.Countable ∧ Dense s

Separable topological space

Informal description

A topological space is called separable if it contains a countable dense subset, meaning there exists a countable set whose closure is the entire space.

TopologicalSpace.exists_countable_dense theorem

[SeparableSpace α] : ∃ s : Set α, s.Countable ∧ Dense s

Full source

theorem exists_countable_dense [SeparableSpace α] : ∃ s : Set α, s.Countable ∧ Dense s :=
  SeparableSpace.exists_countable_dense

Existence of Countable Dense Subset in Separable Spaces

Informal description

In a separable topological space $\alpha$, there exists a countable subset $s \subseteq \alpha$ that is dense in $\alpha$, meaning the closure of $s$ is the entire space.

TopologicalSpace.exists_dense_seq theorem

[SeparableSpace α] [Nonempty α] : ∃ u : ℕ → α, DenseRange u

Full source

/-- A nonempty separable space admits a sequence with dense range. Instead of running `cases` on the
conclusion of this lemma, you might want to use `TopologicalSpace.denseSeq` and
`TopologicalSpace.denseRange_denseSeq`.

If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`. -/
theorem exists_dense_seq [SeparableSpace α] [Nonempty α] : ∃ u : ℕ → α, DenseRange u := by
  obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
  obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs
  exact ⟨u, s_dense.mono hu⟩

Existence of Dense Sequence in Nonempty Separable Spaces

Informal description

In a nonempty separable topological space $\alpha$, there exists a sequence $u \colon \mathbb{N} \to \alpha$ whose range is dense in $\alpha$.

TopologicalSpace.denseSeq definition

[SeparableSpace α] [Nonempty α] : ℕ → α

Full source

/-- A dense sequence in a non-empty separable topological space.

If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`. -/
def denseSeq [SeparableSpace α] [Nonempty α] : ℕ → α :=
  Classical.choose (exists_dense_seq α)

Dense sequence in a separable space

Informal description

Given a nonempty separable topological space $\alpha$, the function `denseSeq` returns a sequence $u \colon \mathbb{N} \to \alpha$ whose range is dense in $\alpha$.

TopologicalSpace.denseRange_denseSeq theorem

[SeparableSpace α] [Nonempty α] : DenseRange (denseSeq α)

Full source

/-- The sequence `TopologicalSpace.denseSeq α` has dense range. -/
@[simp]
theorem denseRange_denseSeq [SeparableSpace α] [Nonempty α] : DenseRange (denseSeq α) :=
  Classical.choose_spec (exists_dense_seq α)

Density of the Canonical Sequence in a Separable Space

Informal description

For any nonempty separable topological space $\alpha$, the sequence $\mathrm{denseSeq}_\alpha \colon \mathbb{N} \to \alpha$ has dense range in $\alpha$.

TopologicalSpace.Countable.to_separableSpace instance

[Countable α] : SeparableSpace α

Full source

instance (priority := 100) Countable.to_separableSpace [Countable α] : SeparableSpace α where
  exists_countable_dense := ⟨Set.univ, Set.countable_univ, dense_univ⟩

Countable Spaces are Separable

Informal description

Every countable topological space is separable.

TopologicalSpace.SeparableSpace.of_denseRange theorem

{ι : Sort _} [Countable ι] (u : ι → α) (hu : DenseRange u) : SeparableSpace α

Full source

/-- If `f` has a dense range and its domain is countable, then its codomain is a separable space.
See also `DenseRange.separableSpace`. -/
theorem SeparableSpace.of_denseRange {ι : Sort _} [Countable ι] (u : ι → α) (hu : DenseRange u) :
    SeparableSpace α :=
  ⟨⟨range u, countable_range u, hu⟩⟩

Separability via Dense Range from Countable Domain

Informal description

Let $\alpha$ be a topological space and $\iota$ be a countable type. Given a function $u \colon \iota \to \alpha$ with dense range (i.e., the closure of the range of $u$ is the entire space $\alpha$), then $\alpha$ is a separable space.

DenseRange.separableSpace theorem

[SeparableSpace α] [TopologicalSpace β] {f : α → β} (h : DenseRange f) (h' : Continuous f) : SeparableSpace β

Full source

/-- If `α` is a separable space and `f : α → β` is a continuous map with dense range, then `β` is
a separable space as well. E.g., the completion of a separable uniform space is separable. -/
protected theorem _root_.DenseRange.separableSpace [SeparableSpace α] [TopologicalSpace β]
    {f : α → β} (h : DenseRange f) (h' : Continuous f) : SeparableSpace β :=
  let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α
  ⟨⟨f '' s, Countable.image s_cnt f, h.dense_image h' s_dense⟩⟩

Separability Preservation under Continuous Maps with Dense Range

Informal description

Let $\alpha$ and $\beta$ be topological spaces, where $\alpha$ is separable. If $f \colon \alpha \to \beta$ is a continuous function with dense range (i.e., the closure of the range of $f$ is $\beta$), then $\beta$ is also separable.

Topology.IsQuotientMap.separableSpace theorem

[SeparableSpace α] [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) : SeparableSpace β

Full source

theorem _root_.Topology.IsQuotientMap.separableSpace [SeparableSpace α] [TopologicalSpace β]
    {f : α → β} (hf : IsQuotientMap f) : SeparableSpace β :=
  hf.surjective.denseRange.separableSpace hf.continuous

Separability Preservation under Quotient Maps

Informal description

Let $\alpha$ and $\beta$ be topological spaces, where $\alpha$ is separable. If $f \colon \alpha \to \beta$ is a quotient map, then $\beta$ is also separable.

TopologicalSpace.instSeparableSpaceProd instance

[TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α × β)

Full source

/-- The product of two separable spaces is a separable space. -/
instance [TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α × β) := by
  rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
  rcases exists_countable_dense β with ⟨t, htc, htd⟩
  exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩

Product of Separable Spaces is Separable

Informal description

The product of two separable topological spaces is separable. That is, if $\alpha$ and $\beta$ are separable topological spaces, then their product $\alpha \times \beta$ is also separable.

TopologicalSpace.instSeparableSpaceForallOfCountable instance

 {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SeparableSpace (X i)] [Countable ι] :
  SeparableSpace (∀ i, X i)

Full source

/-- The product of a countable family of separable spaces is a separable space. -/
instance {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SeparableSpace (X i)]
    [Countable ι] : SeparableSpace (∀ i, X i) := by
  choose t htc htd using (exists_countable_dense <| X ·)
  haveI := fun i ↦ (htc i).to_subtype
  nontriviality ∀ i, X i; inhabit ∀ i, X i
  classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩

Countable Product of Separable Spaces is Separable

Informal description

For any countable index set $\iota$ and any family of separable topological spaces $\{X_i\}_{i \in \iota}$, the product space $\prod_{i \in \iota} X_i$ is separable.

TopologicalSpace.instSeparableSpaceQuot instance

[SeparableSpace α] {r : α → α → Prop} : SeparableSpace (Quot r)

Full source

instance [SeparableSpace α] {r : α → α → Prop} : SeparableSpace (Quot r) :=
  isQuotientMap_quot_mk.separableSpace

Separability of Quotient Spaces

Informal description

For any separable topological space $\alpha$ and any relation $r$ on $\alpha$, the quotient space $\text{Quot } r$ is also separable.

TopologicalSpace.instSeparableSpaceQuotient instance

[SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s)

Full source

instance [SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s) :=
  isQuotientMap_quot_mk.separableSpace

Separability of Quotient Spaces from Separable Spaces

Informal description

For any separable topological space $\alpha$ and any setoid $s$ on $\alpha$, the quotient space $\text{Quotient}\, s$ is also separable.

TopologicalSpace.separableSpace_iff_countable theorem

[DiscreteTopology α] : SeparableSpace α ↔ Countable α

Full source

/-- A topological space with discrete topology is separable iff it is countable. -/
theorem separableSpace_iff_countable [DiscreteTopology α] : SeparableSpaceSeparableSpace α ↔ Countable α := by
  simp [separableSpace_iff, countable_univ_iff]

Separability Equivalence for Discrete Spaces: Countable Type iff Separable Space

Informal description

A topological space $\alpha$ with the discrete topology is separable if and only if the underlying type $\alpha$ is countable.

Pairwise.countable_of_isOpen_disjoint theorem

 [SeparableSpace α] {ι : Type*} {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (ho : ∀ i, IsOpen (s i))
  (hne : ∀ i, (s i).Nonempty) : Countable ι

Full source

/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
theorem _root_.Pairwise.countable_of_isOpen_disjoint [SeparableSpace α] {ι : Type*}
    {s : ι → Set α} (hd : Pairwise (DisjointDisjoint on s)) (ho : ∀ i, IsOpen (s i))
    (hne : ∀ i, (s i).Nonempty) : Countable ι := by
  rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩
  choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)
  have f_inj : Injective f := fun i j hij ↦
    hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩
  have := u_countable.to_subtype
  exact (f_inj.codRestrict hfu).countable

Countability of Index Set for Pairwise Disjoint Nonempty Open Sets in Separable Spaces

Informal description

Let $\alpha$ be a separable topological space, and let $\{s_i\}_{i \in \iota}$ be a family of nonempty open subsets of $\alpha$ indexed by a type $\iota$. If the family is pairwise disjoint (i.e., $s_i \cap s_j = \emptyset$ for all $i \neq j$), then the index set $\iota$ is countable.

Set.PairwiseDisjoint.countable_of_isOpen theorem

 [SeparableSpace α] {ι : Type*} {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i))
  (hne : ∀ i ∈ a, (s i).Nonempty) : a.Countable

Full source

/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
theorem _root_.Set.PairwiseDisjoint.countable_of_isOpen [SeparableSpace α] {ι : Type*}
    {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i))
    (hne : ∀ i ∈ a, (s i).Nonempty) : a.Countable :=
  (h.subtype _ _).countable_of_isOpen_disjoint (Subtype.forall.2 ho) (Subtype.forall.2 hne)

Countability of Pairwise Disjoint Nonempty Open Sets in Separable Spaces

Informal description

Let $\alpha$ be a separable topological space, and let $\{s_i\}_{i \in \iota}$ be a family of nonempty open subsets of $\alpha$ indexed by a subset $a \subseteq \iota$. If the family is pairwise disjoint (i.e., $s_i \cap s_j = \emptyset$ for all $i, j \in a$ with $i \neq j$), then the subset $a$ is countable.

Set.PairwiseDisjoint.countable_of_nonempty_interior theorem

 [SeparableSpace α] {ι : Type*} {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s)
  (ha : ∀ i ∈ a, (interior (s i)).Nonempty) : a.Countable

Full source

/-- In a separable space, a family of disjoint sets with nonempty interiors is countable. -/
theorem _root_.Set.PairwiseDisjoint.countable_of_nonempty_interior [SeparableSpace α] {ι : Type*}
    {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s)
    (ha : ∀ i ∈ a, (interior (s i)).Nonempty) : a.Countable :=
  (h.mono fun _ => interior_subset).countable_of_isOpen (fun _ _ => isOpen_interior) ha

Countability of Pairwise Disjoint Sets with Nonempty Interior in Separable Spaces

Informal description

Let $\alpha$ be a separable topological space, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $\alpha$ indexed by a subset $a \subseteq \iota$. If the family is pairwise disjoint (i.e., $s_i \cap s_j = \emptyset$ for all $i, j \in a$ with $i \neq j$) and each $s_i$ has nonempty interior, then the subset $a$ is countable.

TopologicalSpace.IsSeparable definition

(s : Set α)

Full source

/-- A set `s` in a topological space is separable if it is contained in the closure of a countable
set `c`. Beware that this definition does not require that `c` is contained in `s` (to express the
latter, use `TopologicalSpace.SeparableSpace s` or
`TopologicalSpace.IsSeparable (univ : Set s))`. In metric spaces, the two definitions are
equivalent, see `TopologicalSpace.IsSeparable.separableSpace`. -/
def IsSeparable (s : Set α) :=
  ∃ c : Set α, c.Countable ∧ s ⊆ closure c

Separable set in a topological space

Informal description

A set $ s $ in a topological space is called *separable* if there exists a countable set $ c $ such that $ s $ is contained in the closure of $ c $. Note that $ c $ is not required to be a subset of $ s $.

TopologicalSpace.IsSeparable.mono theorem

{s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u

Full source

theorem IsSeparable.mono {s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u := by
  rcases hs with ⟨c, c_count, hs⟩
  exact ⟨c, c_count, hu.trans hs⟩

Subset of a Separable Set is Separable

Informal description

Let $s$ and $u$ be subsets of a topological space $\alpha$. If $s$ is separable and $u \subseteq s$, then $u$ is also separable.

TopologicalSpace.IsSeparable.iUnion theorem

{ι : Sort*} [Countable ι] {s : ι → Set α} (hs : ∀ i, IsSeparable (s i)) : IsSeparable (⋃ i, s i)

Full source

theorem IsSeparable.iUnion {ι : Sort*} [Countable ι] {s : ι → Set α}
    (hs : ∀ i, IsSeparable (s i)) : IsSeparable (⋃ i, s i) := by
  choose c hc h'c using hs
  refine ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩
  exact (h'c i).trans (closure_mono (subset_iUnion _ i))

Separability of Countable Union of Separable Sets

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of sets in a topological space $\alpha$, where the index set $\iota$ is countable. If each set $s_i$ is separable (i.e., contained in the closure of some countable set), then their union $\bigcup_{i \in \iota} s_i$ is also separable.

TopologicalSpace.isSeparable_iUnion theorem

{ι : Sort*} [Countable ι] {s : ι → Set α} : IsSeparable (⋃ i, s i) ↔ ∀ i, IsSeparable (s i)

Full source

@[simp]
theorem isSeparable_iUnion {ι : Sort*} [Countable ι] {s : ι → Set α} :
    IsSeparableIsSeparable (⋃ i, s i) ↔ ∀ i, IsSeparable (s i) :=
  ⟨fun h i ↦ h.mono <| subset_iUnion s i, .iUnion⟩

Separability of Countable Union of Sets in Topological Space

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of sets in a topological space $\alpha$, where the index set $\iota$ is countable. The union $\bigcup_{i \in \iota} s_i$ is separable if and only if each set $s_i$ is separable. Here, a set is called *separable* if it is contained in the closure of some countable set.

TopologicalSpace.isSeparable_union theorem

{s t : Set α} : IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Full source

@[simp]
theorem isSeparable_union {s t : Set α} : IsSeparableIsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t := by
  simp [union_eq_iUnion, and_comm]

Separability of Union of Sets in Topological Space

Informal description

For any two sets $s$ and $t$ in a topological space, the union $s \cup t$ is separable if and only if both $s$ and $t$ are separable. Here, a set is called *separable* if it is contained in the closure of some countable set.

TopologicalSpace.IsSeparable.union theorem

{s u : Set α} (hs : IsSeparable s) (hu : IsSeparable u) : IsSeparable (s ∪ u)

Full source

theorem IsSeparable.union {s u : Set α} (hs : IsSeparable s) (hu : IsSeparable u) :
    IsSeparable (s ∪ u) :=
  isSeparable_union.2 ⟨hs, hu⟩

Union of Separable Sets is Separable

Informal description

For any two sets $s$ and $u$ in a topological space, if $s$ is separable and $u$ is separable, then their union $s \cup u$ is also separable. Here, a set is called *separable* if it is contained in the closure of some countable set.

TopologicalSpace.isSeparable_closure theorem

: IsSeparable (closure s) ↔ IsSeparable s

Full source

@[simp]
theorem isSeparable_closure : IsSeparableIsSeparable (closure s) ↔ IsSeparable s := by
  simp only [IsSeparable, isClosed_closure.closure_subset_iff]

Separability of a Set and Its Closure

Informal description

For any subset $s$ of a topological space, the closure $\overline{s}$ is separable if and only if $s$ is separable. Here, a set is called *separable* if it is contained in the closure of some countable set.

Set.Countable.isSeparable theorem

{s : Set α} (hs : s.Countable) : IsSeparable s

Full source

theorem _root_.Set.Countable.isSeparable {s : Set α} (hs : s.Countable) : IsSeparable s :=
  ⟨s, hs, subset_closure⟩

Countable Sets are Separable in Topological Spaces

Informal description

For any countable subset $s$ of a topological space $\alpha$, the set $s$ is separable, i.e., there exists a countable set whose closure contains $s$.

Set.Finite.isSeparable theorem

{s : Set α} (hs : s.Finite) : IsSeparable s

Full source

theorem _root_.Set.Finite.isSeparable {s : Set α} (hs : s.Finite) : IsSeparable s :=
  hs.countable.isSeparable

Finite Sets are Separable in Topological Spaces

Informal description

For any finite subset $s$ of a topological space $\alpha$, the set $s$ is separable, i.e., there exists a countable set whose closure contains $s$.

TopologicalSpace.IsSeparable.univ_pi theorem

 {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)} [∀ i, TopologicalSpace (X i)]
  (h : ∀ i, IsSeparable (s i)) : IsSeparable (univ.pi s)

Full source

theorem IsSeparable.univ_pi {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)}
    [∀ i, TopologicalSpace (X i)] (h : ∀ i, IsSeparable (s i)) :
    IsSeparable (univ.pi s) := by
  classical
  rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
  · rw [he]
    exact countable_empty.isSeparable
  · choose c c_count hc using h
    haveI := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2

Separability of Countable Product of Separable Sets

Informal description

Let $\iota$ be a countable index set and $\{X_i\}_{i \in \iota}$ a family of topological spaces. For each $i \in \iota$, let $s_i \subseteq X_i$ be a separable subset. Then the product set $\prod_{i \in \iota} s_i$ is separable in the product topology on $\prod_{i \in \iota} X_i$.

TopologicalSpace.isSeparable_pi theorem

 {ι : Type*} [Countable ι] {α : ι → Type*} {s : ∀ i, Set (α i)} [∀ i, TopologicalSpace (α i)]
  (h : ∀ i, IsSeparable (s i)) : IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i}

Full source

lemma isSeparable_pi {ι : Type*} [Countable ι] {α : ι → Type*} {s : ∀ i, Set (α i)}
    [∀ i, TopologicalSpace (α i)] (h : ∀ i, IsSeparable (s i)) :
    IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i} := by
  simpa only [← mem_univ_pi] using IsSeparable.univ_pi h

Separability of Countable Product of Separable Sets in Function Space

Informal description

Let $\iota$ be a countable index set and $\{\alpha_i\}_{i \in \iota}$ a family of topological spaces. For each $i \in \iota$, let $s_i \subseteq \alpha_i$ be a separable subset. Then the set of all functions $f \in \prod_{i \in \iota} \alpha_i$ such that $f(i) \in s_i$ for every $i \in \iota$ is separable in the product topology on $\prod_{i \in \iota} \alpha_i$.

TopologicalSpace.IsSeparable.prod theorem

 {β : Type*} [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :
  IsSeparable (s ×ˢ t)

Full source

lemma IsSeparable.prod {β : Type*} [TopologicalSpace β]
    {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :
    IsSeparable (s ×ˢ t) := by
  rcases hs with ⟨cs, cs_count, hcs⟩
  rcases ht with ⟨ct, ct_count, hct⟩
  refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
  rw [closure_prod_eq]
  gcongr

Separability of Cartesian Product of Separable Sets

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $s \subseteq \alpha$ and $t \subseteq \beta$ be separable sets. Then the Cartesian product $s \times t$ is also separable.

TopologicalSpace.IsSeparable.image theorem

 {β : Type*} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s) {f : α → β} (hf : Continuous f) :
  IsSeparable (f '' s)

Full source

theorem IsSeparable.image {β : Type*} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s)
    {f : α → β} (hf : Continuous f) : IsSeparable (f '' s) := by
  rcases hs with ⟨c, c_count, hc⟩
  refine ⟨f '' c, c_count.image _, ?_⟩
  rw [image_subset_iff]
  exact hc.trans (closure_subset_preimage_closure_image hf)

Continuous Image of Separable Set is Separable

Informal description

Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a separable subset, and $f \colon X \to Y$ a continuous function. Then the image $f(s) \subseteq Y$ is separable.

Dense.isSeparable_iff theorem

(hs : Dense s) : IsSeparable s ↔ SeparableSpace α

Full source

theorem _root_.Dense.isSeparable_iff (hs : Dense s) :
    IsSeparableIsSeparable s ↔ SeparableSpace α := by
  simp_rw [IsSeparable, separableSpace_iff, dense_iff_closure_eq, ← univ_subset_iff,
    ← hs.closure_eq, isClosed_closure.closure_subset_iff]

Dense Set Separability Criterion: $s$ dense implies $s$ separable iff $\alpha$ separable

Informal description

For a dense subset $s$ of a topological space $\alpha$, the set $s$ is separable if and only if the entire space $\alpha$ is separable. In other words, $s$ is separable (i.e., contained in the closure of some countable set) if and only if $\alpha$ has a countable dense subset.

TopologicalSpace.isSeparable_univ_iff theorem

: IsSeparable (univ : Set α) ↔ SeparableSpace α

Full source

theorem isSeparable_univ_iff : IsSeparableIsSeparable (univ : Set α) ↔ SeparableSpace α :=
  dense_univ.isSeparable_iff

Separability of Universal Set Equivalence: $\text{IsSeparable}(\text{univ}) \leftrightarrow \text{SeparableSpace}(\alpha)$

Informal description

The universal set in a topological space $\alpha$ is separable if and only if $\alpha$ is a separable space. In other words, there exists a countable subset whose closure contains all elements of $\alpha$ if and only if $\alpha$ has a countable dense subset.

TopologicalSpace.isSeparable_range theorem

[TopologicalSpace β] [SeparableSpace α] {f : α → β} (hf : Continuous f) : IsSeparable (range f)

Full source

theorem isSeparable_range [TopologicalSpace β] [SeparableSpace α] {f : α → β} (hf : Continuous f) :
    IsSeparable (range f) :=
  image_univ (f := f) ▸ (isSeparable_univ_iff.2 ‹_›).image hf

Continuous Image of Separable Space Has Separable Range

Informal description

Let $X$ and $Y$ be topological spaces, where $X$ is separable. For any continuous function $f \colon X \to Y$, the range of $f$ is a separable subset of $Y$.

TopologicalSpace.IsSeparable.of_subtype theorem

(s : Set α) [SeparableSpace s] : IsSeparable s

Full source

theorem IsSeparable.of_subtype (s : Set α) [SeparableSpace s] : IsSeparable s := by
  simpa using isSeparable_range (continuous_subtype_val (p := (· ∈ s)))

Separability of Subspace Implies Separability of Subset

Informal description

For any subset $s$ of a topological space $\alpha$, if the subspace topology on $s$ is separable, then $s$ is a separable set in $\alpha$.

TopologicalSpace.IsSeparable.of_separableSpace theorem

[h : SeparableSpace α] (s : Set α) : IsSeparable s

Full source

theorem IsSeparable.of_separableSpace [h : SeparableSpace α] (s : Set α) : IsSeparable s :=
  IsSeparable.mono (isSeparable_univ_iff.2 h) (subset_univ _)

Subsets of a separable space are separable

Informal description

If a topological space $\alpha$ is separable, then any subset $s$ of $\alpha$ is separable.

IsTopologicalBasis.iInf theorem

 {β : Type*} {ι : Type*} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)}
  (h_basis : ∀ i, IsTopologicalBasis (t := t i) (T i)) :
  IsTopologicalBasis (t := ⨅ i, t i) {S | ∃ (U : ι → Set β) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}

Full source

protected theorem IsTopologicalBasis.iInf {β : Type*} {ι : Type*} {t : ι → TopologicalSpace β}
    {T : ι → Set (Set β)} (h_basis : ∀ i, IsTopologicalBasis (t := t i) (T i)) :
    IsTopologicalBasis (t := ⨅ i, t i)
      { S | ∃ (U : ι → Set β) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i ∈ F, U i } := by
  let _ := ⨅ i, t i
  refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
  · rintro - ⟨U, F, hU, rfl⟩
    refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)
  · intro a u ha hu
    rcases (nhds_iInf (t := t) (a := a)).symm ▸ hasBasis_iInf'
      (fun i ↦ (h_basis i).nhds_hasBasis (t := t i)) |>.mem_iff.1 (hu.mem_nhds ha)
      with ⟨⟨F, U⟩, ⟨hF, hU⟩, hUu⟩
    refine ⟨_, ⟨U, hF.toFinset, ?_, rfl⟩, ?_, ?_⟩ <;> simp only [Finite.mem_toFinset, mem_iInter]
    · exact fun i hi ↦ (hU i hi).1
    · exact fun i hi ↦ (hU i hi).2
    · exact hUu

Topological Basis for Infimum Topology via Finite Intersections of Basis Sets

Informal description

Let $\beta$ be a type, $\iota$ be an index type, and for each $i \in \iota$, let $t_i$ be a topology on $\beta$ with a topological basis $T_i$. Then the collection of all finite intersections of sets from the bases $T_i$ forms a topological basis for the infimum topology $\bigsqcap_i t_i$ on $\beta$. More precisely, the basis consists of all sets of the form $\bigcap_{i \in F} U_i$, where $F$ is a finite subset of $\iota$ and for each $i \in F$, $U_i \in T_i$.

IsTopologicalBasis.iInf_induced theorem

 {β : Type*} {ι : Type*} {X : ι → Type*} [t : Π i, TopologicalSpace (X i)] {T : Π i, Set (Set (X i))}
  (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :
  IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))
    {S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i}

Full source

theorem IsTopologicalBasis.iInf_induced {β : Type*} {ι : Type*} {X : ι → Type*}
    [t : Π i, TopologicalSpace (X i)] {T : Π i, Set (Set (X i))}
    (cond : ∀ i, IsTopologicalBasis (T i)) (f : Π i, β → X i) :
    IsTopologicalBasis (t := ⨅ i, induced (f i) (t i))
      { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
        (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ (i) (_ : i ∈ F), f i ⁻¹' U i } := by
  convert IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S
  constructor <;> rintro ⟨U, F, hUT, hSU⟩
  · exact ⟨fun i ↦ (f i) ⁻¹' (U i), F, fun i hi ↦ mem_image_of_mem _ (hUT i hi), hSU⟩
  · choose! U' hU' hUU' using hUT
    exact ⟨U', F, hU', hSU ▸ (.symm <| iInter₂_congr hUU')⟩

Topological Basis for Infimum of Induced Topologies via Finite Intersections of Preimages

Informal description

Let $\{X_i\}_{i \in \iota}$ be a family of topological spaces, each equipped with a topological basis $T_i$. Given a family of functions $f_i : \beta \to X_i$, the collection of all finite intersections of preimages $\bigcap_{i \in F} f_i^{-1}(U_i)$, where $F$ is a finite subset of $\iota$ and $U_i \in T_i$ for each $i \in F$, forms a topological basis for the infimum topology on $\beta$ induced by the family $\{f_i\}_{i \in \iota}$.

isTopologicalBasis_pi theorem

 {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {T : ∀ i, Set (Set (X i))}
  (cond : ∀ i, IsTopologicalBasis (T i)) :
  IsTopologicalBasis {S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U}

Full source

theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    {T : ∀ i, Set (Set (X i))} (cond : ∀ i, IsTopologicalBasis (T i)) :
    IsTopologicalBasis { S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι),
      (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U } := by
  simpa only [Set.pi_def] using IsTopologicalBasis.iInf_induced cond eval

Product Topology Basis from Finite Products of Basis Sets

Informal description

Let $\{X_i\}_{i \in \iota}$ be a family of topological spaces, each with a topological basis $T_i$. Then the collection of all sets of the form $\prod_{i \in F} U_i$, where $F$ is a finite subset of $\iota$ and $U_i \in T_i$ for each $i \in F$, forms a topological basis for the product topology on $\prod_{i \in \iota} X_i$.

isTopologicalBasis_singletons theorem

(α : Type*) [TopologicalSpace α] [DiscreteTopology α] : IsTopologicalBasis {s | ∃ x : α, (s : Set α) = { x }}

Full source

theorem isTopologicalBasis_singletons (α : Type*) [TopologicalSpace α] [DiscreteTopology α] :
    IsTopologicalBasis { s | ∃ x : α, (s : Set α) = {x} } :=
  isTopologicalBasis_of_isOpen_of_nhds (fun _ _ => isOpen_discrete _) fun x _ hx _ =>
    ⟨{x}, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩

Singletons Form a Basis in Discrete Topology

Informal description

For any type $\alpha$ equipped with the discrete topology, the collection of all singleton sets $\{\{x\} \mid x \in \alpha\}$ forms a topological basis.

isTopologicalBasis_subtype theorem

 {α : Type*} [TopologicalSpace α] {B : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) :
  IsTopologicalBasis (Set.preimage (Subtype.val (p := p)) '' B)

Full source

theorem isTopologicalBasis_subtype
    {α : Type*} [TopologicalSpace α] {B : Set (Set α)}
    (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) :
    IsTopologicalBasis (Set.preimageSet.preimage (Subtype.val (p := p)) '' B) :=
  h.isInducing ⟨rfl⟩

Subspace Topology Basis from Preimage of Basis

Informal description

Let $\alpha$ be a topological space with a topological basis $B$, and let $p : \alpha \to \text{Prop}$ be a predicate on $\alpha$. Then the collection of preimages $\{\text{Subtype.val}^{-1}(U) \mid U \in B\}$ forms a topological basis for the subspace topology on $\{x \in \alpha \mid p(x)\}$.

isOpenMap_eval theorem

(i : ι) : IsOpenMap (Function.eval i : (∀ i, π i) → π i)

Full source

lemma isOpenMap_eval (i : ι) : IsOpenMap (Function.eval i : (∀ i, π i) → π i) := by
  classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_not_mem (mod_cast hi), if_pos h]
    exact isOpen_univ

Openness of Evaluation Maps in Product Topology

Informal description

For any index $i$ in the index set $\iota$, the evaluation map $\text{eval}_i : \prod_{j \in \iota} \pi_j \to \pi_i$ is an open map with respect to the product topology on $\prod_{j \in \iota} \pi_j$ and the topology on $\pi_i$.

Dense.exists_countable_dense_subset theorem

 {α : Type*} [TopologicalSpace α] {s : Set α} [SeparableSpace s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t

Full source

theorem Dense.exists_countable_dense_subset {α : Type*} [TopologicalSpace α] {s : Set α}
    [SeparableSpace s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t :=
  let ⟨t, htc, htd⟩ := exists_countable_dense s
  ⟨(↑) '' t, Subtype.coe_image_subset s t, htc.image Subtype.val,
    hs.denseRange_val.dense_image continuous_subtype_val htd⟩

Existence of Countable Dense Subset in Dense Subspace of Separable Space

Informal description

Let $X$ be a topological space and $s \subseteq X$ a dense subset. If the subspace topology on $s$ is separable, then there exists a countable subset $t \subseteq s$ that is dense in $X$.

Dense.exists_countable_dense_subset_bot_top theorem

 {α : Type*} [TopologicalSpace α] [PartialOrder α] {s : Set α} [SeparableSpace s] (hs : Dense s) :
  ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∈ s → x ∈ t) ∧ ∀ x, IsTop x → x ∈ s → x ∈ t

Full source

/-- Let `s` be a dense set in a topological space `α` with partial order structure. If `s` is a
separable space (e.g., if `α` has a second countable topology), then there exists a countable
dense subset `t ⊆ s` such that `t` contains bottom/top element of `α` when they exist and belong
to `s`. For a dense subset containing neither bot nor top elements, see
`Dense.exists_countable_dense_subset_no_bot_top`. -/
theorem Dense.exists_countable_dense_subset_bot_top {α : Type*} [TopologicalSpace α]
    [PartialOrder α] {s : Set α} [SeparableSpace s] (hs : Dense s) :
    ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ x, IsBot x → x ∈ s → x ∈ t) ∧
      ∀ x, IsTop x → x ∈ s → x ∈ t := by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
  refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
  exacts [inter_subset_right,
    (htc.union ((countable_isBot α).union (countable_isTop α))).mono inter_subset_left,
    htd.mono (subset_inter subset_union_left hts), fun x hx hxs => ⟨Or.inr <| Or.inl hx, hxs⟩,
    fun x hx hxs => ⟨Or.inr <| Or.inr hx, hxs⟩]

Existence of Countable Dense Subset Containing Extremal Elements in a Dense Subspace of a Separable Ordered Topological Space

Informal description

Let $\alpha$ be a topological space with a partial order, and let $s \subseteq \alpha$ be a dense subset such that the subspace topology on $s$ is separable. Then there exists a countable subset $t \subseteq s$ that is dense in $\alpha$ and satisfies the following properties: 1. If $x \in s$ is a bottom element of $\alpha$ (i.e., $x \leq y$ for all $y \in \alpha$), then $x \in t$. 2. If $x \in s$ is a top element of $\alpha$ (i.e., $y \leq x$ for all $y \in \alpha$), then $x \in t$.

separableSpace_univ instance

{α : Type*} [TopologicalSpace α] [SeparableSpace α] : SeparableSpace (univ : Set α)

Full source

instance separableSpace_univ {α : Type*} [TopologicalSpace α] [SeparableSpace α] :
    SeparableSpace (univ : Set α) :=
  (Equiv.Set.univ α).symm.surjective.denseRange.separableSpace (continuous_id.subtype_mk _)

Separability of the Universal Set in a Separable Space

Informal description

For any topological space $\alpha$ that is separable, the universal set $\text{univ} \subseteq \alpha$ (equipped with the subspace topology) is also separable.

exists_countable_dense_bot_top theorem

 (α : Type*) [TopologicalSpace α] [SeparableSpace α] [PartialOrder α] :
  ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∈ s) ∧ ∀ x, IsTop x → x ∈ s

Full source

/-- If `α` is a separable topological space with a partial order, then there exists a countable
dense set `s : Set α` that contains those of both bottom and top elements of `α` that actually
exist. For a dense set containing neither bot nor top elements, see
`exists_countable_dense_no_bot_top`. -/
theorem exists_countable_dense_bot_top (α : Type*) [TopologicalSpace α] [SeparableSpace α]
    [PartialOrder α] :
    ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∈ s) ∧ ∀ x, IsTop x → x ∈ s := by
  simpa using dense_univ.exists_countable_dense_subset_bot_top

Existence of Countable Dense Subset Containing Extremal Elements in a Separable Ordered Space

Informal description

Let $\alpha$ be a separable topological space with a partial order. Then there exists a countable dense subset $s \subseteq \alpha$ such that: 1. If $\alpha$ has a bottom element $x$ (i.e., $x \leq y$ for all $y \in \alpha$), then $x \in s$. 2. If $\alpha$ has a top element $x$ (i.e., $y \leq x$ for all $y \in \alpha$), then $x \in s$.

FirstCountableTopology structure

Full source

/-- A first-countable space is one in which every point has a
  countable neighborhood basis. -/
class _root_.FirstCountableTopology : Prop where
  /-- The filter `𝓝 a` is countably generated for all points `a`. -/
  nhds_generated_countable : ∀ a : α, (𝓝 a).IsCountablyGenerated

First-countable topological space

Informal description

A first-countable topological space is one in which every point has a countable neighborhood basis. That is, for every point $ x $ in the space, there exists a countable collection of open neighborhoods of $ x $ such that any neighborhood of $ x $ contains some member of this collection.

TopologicalSpace.firstCountableTopology_induced theorem

 (α β : Type*) [t : TopologicalSpace β] [FirstCountableTopology β] (f : α → β) : @FirstCountableTopology α (t.induced f)

Full source

/-- If `β` is a first-countable space, then its induced topology via `f` on `α` is also
first-countable. -/
theorem firstCountableTopology_induced (α β : Type*) [t : TopologicalSpace β]
    [FirstCountableTopology β] (f : α → β) : @FirstCountableTopology α (t.induced f) :=
  let _ := t.induced f
  ⟨fun x ↦ nhds_induced f x ▸ inferInstance⟩

First-Countability is Preserved under Induced Topology

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a topology $t$ that is first-countable. For any function $f : \alpha \to \beta$, the induced topology on $\alpha$ (defined as the coarsest topology making $f$ continuous) is also first-countable.

TopologicalSpace.Subtype.firstCountableTopology instance

(s : Set α) [FirstCountableTopology α] : FirstCountableTopology s

Full source

instance Subtype.firstCountableTopology (s : Set α) [FirstCountableTopology α] :
    FirstCountableTopology s :=
  firstCountableTopology_induced s α (↑)

First-Countability of Subspace Topology

Informal description

For any subset $s$ of a topological space $\alpha$ that is first-countable, the subspace topology on $s$ is also first-countable.

Topology.IsInducing.firstCountableTopology theorem

 {β : Type*} [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsInducing f) : FirstCountableTopology α

Full source

protected theorem _root_.Topology.IsInducing.firstCountableTopology {β : Type*}
    [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsInducing f) :
    FirstCountableTopology α := by
  rw [hf.1]
  exact firstCountableTopology_induced α β f

First-Countability is Preserved under Induced Topology via Inducing Function

Informal description

Let $\beta$ be a topological space that is first-countable, and let $f : \alpha \to \beta$ be a function that induces the topology on $\alpha$ (i.e., the topology on $\alpha$ is the coarsest topology making $f$ continuous). Then $\alpha$ is also first-countable.

Topology.IsEmbedding.firstCountableTopology theorem

 {β : Type*} [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) : FirstCountableTopology α

Full source

protected theorem _root_.Topology.IsEmbedding.firstCountableTopology {β : Type*}
    [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) :
    FirstCountableTopology α :=
  hf.1.firstCountableTopology

First-countability is preserved under embeddings

Informal description

Let $\beta$ be a first-countable topological space and $f : \alpha \to \beta$ be an embedding (i.e., a homeomorphism onto its image). Then the topological space $\alpha$ is also first-countable.

TopologicalSpace.FirstCountableTopology.tendsto_subseq theorem

 [FirstCountableTopology α] {u : ℕ → α} {x : α} (hx : MapClusterPt x atTop u) :
  ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x)

Full source

/-- In a first-countable space, a cluster point `x` of a sequence
is the limit of some subsequence. -/
theorem tendsto_subseq [FirstCountableTopology α] {u : ℕ → α} {x : α}
    (hx : MapClusterPt x atTop u) : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ Tendsto (u ∘ ψ) atTop (𝓝 x) :=
  subseq_tendsto_of_neBot hx

Subsequence Convergence in First-Countable Spaces

Informal description

In a first-countable topological space $\alpha$, if $x$ is a cluster point of a sequence $u : \mathbb{N} \to \alpha$, then there exists a strictly increasing function $\psi : \mathbb{N} \to \mathbb{N}$ such that the subsequence $u \circ \psi$ converges to $x$.

TopologicalSpace.instFirstCountableTopologyProd instance

{β} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] : FirstCountableTopology (α × β)

Full source

instance {β} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] :
    FirstCountableTopology (α × β) :=
  ⟨fun ⟨x, y⟩ => by rw [nhds_prod_eq]; infer_instance⟩

First-Countability of Product Spaces

Informal description

The product of two first-countable topological spaces is first-countable.

TopologicalSpace.instFirstCountableTopologyForallOfCountable instance

 {ι : Type*} {π : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (π i)] [∀ i, FirstCountableTopology (π i)] :
  FirstCountableTopology (∀ i, π i)

Full source

instance {ι : Type*} {π : ι → Type*} [Countable ι] [∀ i, TopologicalSpace (π i)]
    [∀ i, FirstCountableTopology (π i)] : FirstCountableTopology (∀ i, π i) :=
  ⟨fun f => by rw [nhds_pi]; infer_instance⟩

First-Countability of Countable Product Spaces

Informal description

For any countable index set $\iota$ and family of topological spaces $\{\pi_i\}_{i \in \iota}$, if each $\pi_i$ is first-countable, then the product space $\prod_{i \in \iota} \pi_i$ is also first-countable.

TopologicalSpace.isCountablyGenerated_nhdsWithin instance

(x : α) [IsCountablyGenerated (𝓝 x)] (s : Set α) : IsCountablyGenerated (𝓝[s] x)

Full source

instance isCountablyGenerated_nhdsWithin (x : α) [IsCountablyGenerated (𝓝 x)] (s : Set α) :
    IsCountablyGenerated (𝓝[s] x) :=
  Inf.isCountablyGenerated _ _

Countable Generation of Neighborhood Filters within Subsets

Informal description

For any point $x$ in a topological space $\alpha$ where the neighborhood filter $\mathcal{N}(x)$ is countably generated, and for any subset $s \subseteq \alpha$, the neighborhood filter $\mathcal{N}_s(x)$ within $s$ is also countably generated.

SecondCountableTopology structure

Full source

/-- A second-countable space is one with a countable basis. -/
class _root_.SecondCountableTopology : Prop where
  /-- There exists a countable set of sets that generates the topology. -/
  is_open_generated_countable : ∃ b : Set (Set α), b.Countable ∧ t = TopologicalSpace.generateFrom b

Second-countable topological space

Informal description

A topological space is called second-countable if it has a countable basis, meaning there exists a countable collection of open sets such that every open set in the space can be expressed as a union of sets from this collection.

TopologicalSpace.IsTopologicalBasis.secondCountableTopology theorem

{b : Set (Set α)} (hb : IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α

Full source

protected theorem IsTopologicalBasis.secondCountableTopology {b : Set (Set α)}
    (hb : IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α :=
  ⟨⟨b, hc, hb.eq_generateFrom⟩⟩

Countable Basis Implies Second-Countability

Informal description

Let $\alpha$ be a topological space with a basis $b$ of open sets. If $b$ is countable, then $\alpha$ is second-countable.

TopologicalSpace.SecondCountableTopology.mk' theorem

{α} {b : Set (Set α)} (hc : b.Countable) : @SecondCountableTopology α (generateFrom b)

Full source

lemma SecondCountableTopology.mk' {α} {b : Set (Set α)} (hc : b.Countable) :
    @SecondCountableTopology α (generateFrom b) :=
  @SecondCountableTopology.mk α (generateFrom b) ⟨b, hc, rfl⟩

Second-countability of the topology generated by a countable basis

Informal description

Let $\alpha$ be a type and $b$ be a countable collection of subsets of $\alpha$. Then the topology generated by $b$ is second-countable.

Finite.toSecondCountableTopology instance

[Finite α] : SecondCountableTopology α

Full source

instance _root_.Finite.toSecondCountableTopology [Finite α] : SecondCountableTopology α where
  is_open_generated_countable :=
    ⟨_, {U | IsOpen U}.to_countable, TopologicalSpace.isTopologicalBasis_opens.eq_generateFrom⟩

Finite Spaces are Second-Countable

Informal description

Every finite topological space is second-countable.

TopologicalSpace.exists_countable_basis theorem

[SecondCountableTopology α] : ∃ b : Set (Set α), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

Full source

theorem exists_countable_basis [SecondCountableTopology α] :
    ∃ b : Set (Set α), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b := by
  obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
  refine ⟨_, ?_, not_mem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
  exacts [((countable_setOf_finite_subset hb₁).image _).mono diff_subset, rfl]

Existence of Countable Basis in Second-Countable Spaces

Informal description

If a topological space $\alpha$ is second-countable, then there exists a countable collection $b$ of subsets of $\alpha$ that forms a topological basis and does not contain the empty set. That is, $b$ is countable, $\emptyset \notin b$, and every open set in $\alpha$ can be expressed as a union of sets from $b$.

TopologicalSpace.countableBasis definition

[SecondCountableTopology α] : Set (Set α)

Full source

/-- A countable topological basis of `α`. -/
def countableBasis [SecondCountableTopology α] : Set (Set α) :=
  (exists_countable_basis α).choose

Countable topological basis of a second-countable space

Informal description

Given a second-countable topological space $\alpha$, the set `countableBasis α` is a countable collection of open sets that forms a topological basis for $\alpha$. This means every open set in $\alpha$ can be expressed as a union of sets from `countableBasis α`.

TopologicalSpace.countable_countableBasis theorem

[SecondCountableTopology α] : (countableBasis α).Countable

Full source

theorem countable_countableBasis [SecondCountableTopology α] : (countableBasis α).Countable :=
  (exists_countable_basis α).choose_spec.1

Countability of the Basis in Second-Countable Spaces

Informal description

For any second-countable topological space $\alpha$, the set `countableBasis α` is countable.

TopologicalSpace.encodableCountableBasis instance

[SecondCountableTopology α] : Encodable (countableBasis α)

Full source

instance encodableCountableBasis [SecondCountableTopology α] : Encodable (countableBasis α) :=
  (countable_countableBasis α).toEncodable

Encodability of the Countable Basis in Second-Countable Spaces

Informal description

For any second-countable topological space $\alpha$, the countable basis `countableBasis α` is encodable. This means there exists an explicit encoding function from the basis sets to the natural numbers, along with a partial inverse decoding function.

TopologicalSpace.empty_nmem_countableBasis theorem

[SecondCountableTopology α] : ∅ ∉ countableBasis α

Full source

theorem empty_nmem_countableBasis [SecondCountableTopology α] : ∅∅ ∉ countableBasis α :=
  (exists_countable_basis α).choose_spec.2.1

Empty Set Exclusion from Countable Basis in Second-Countable Spaces

Informal description

In a second-countable topological space $\alpha$, the empty set is not contained in the countable basis `countableBasis α$.

TopologicalSpace.isBasis_countableBasis theorem

[SecondCountableTopology α] : IsTopologicalBasis (countableBasis α)

Full source

theorem isBasis_countableBasis [SecondCountableTopology α] :
    IsTopologicalBasis (countableBasis α) :=
  (exists_countable_basis α).choose_spec.2.2

Countable Basis Property in Second-Countable Spaces

Informal description

For a second-countable topological space $\alpha$, the collection `countableBasis α` forms a topological basis. That is, every open set in $\alpha$ can be expressed as a union of sets from `countableBasis α`.

TopologicalSpace.isOpen_of_mem_countableBasis theorem

[SecondCountableTopology α] {s : Set α} (hs : s ∈ countableBasis α) : IsOpen s

Full source

theorem isOpen_of_mem_countableBasis [SecondCountableTopology α] {s : Set α}
    (hs : s ∈ countableBasis α) : IsOpen s :=
  (isBasis_countableBasis α).isOpen hs

Openness of Sets in a Countable Basis

Informal description

Let $\alpha$ be a second-countable topological space. For any set $s$ in the countable basis of $\alpha$, $s$ is open in $\alpha$.

TopologicalSpace.nonempty_of_mem_countableBasis theorem

[SecondCountableTopology α] {s : Set α} (hs : s ∈ countableBasis α) : s.Nonempty

Full source

theorem nonempty_of_mem_countableBasis [SecondCountableTopology α] {s : Set α}
    (hs : s ∈ countableBasis α) : s.Nonempty :=
  nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs <| empty_nmem_countableBasis α

Nonemptiness of Basis Sets in Second-Countable Spaces

Informal description

In a second-countable topological space $\alpha$, every nonempty set $s$ in the countable basis `countableBasis α` is nonempty. That is, if $s \in \text{countableBasis} \alpha$, then $s \neq \emptyset$.

TopologicalSpace.SecondCountableTopology.to_firstCountableTopology instance

[SecondCountableTopology α] : FirstCountableTopology α

Full source

instance (priority := 100) SecondCountableTopology.to_firstCountableTopology
    [SecondCountableTopology α] : FirstCountableTopology α :=
  ⟨fun _ => HasCountableBasis.isCountablyGenerated <|
      ⟨(isBasis_countableBasis α).nhds_hasBasis,
        (countable_countableBasis α).mono inter_subset_left⟩⟩

Second-Countable Implies First-Countable

Informal description

Every second-countable topological space is also first-countable.

TopologicalSpace.secondCountableTopology_induced theorem

 (α β) [t : TopologicalSpace β] [SecondCountableTopology β] (f : α → β) : @SecondCountableTopology α (t.induced f)

Full source

/-- If `β` is a second-countable space, then its induced topology via
`f` on `α` is also second-countable. -/
theorem secondCountableTopology_induced (α β) [t : TopologicalSpace β] [SecondCountableTopology β]
    (f : α → β) : @SecondCountableTopology α (t.induced f) := by
  rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
  letI := t.induced f
  refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
  rw [eq, induced_generateFrom_eq]

Second-Countability of Induced Topology from Second-Countable Space

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ being second-countable. Given any function $f : \alpha \to \beta$, the induced topology on $\alpha$ via $f$ is also second-countable.

TopologicalSpace.Subtype.secondCountableTopology instance

(s : Set α) [SecondCountableTopology α] : SecondCountableTopology s

Full source

instance Subtype.secondCountableTopology (s : Set α) [SecondCountableTopology α] :
    SecondCountableTopology s :=
  secondCountableTopology_induced s α (↑)

Subspace of Second-Countable Space is Second-Countable

Informal description

For any subset $s$ of a second-countable topological space $\alpha$, the subspace topology on $s$ is also second-countable.

TopologicalSpace.secondCountableTopology_iInf theorem

 {α ι} [Countable ι] {t : ι → TopologicalSpace α} (ht : ∀ i, @SecondCountableTopology α (t i)) :
  @SecondCountableTopology α (⨅ i, t i)

Full source

lemma secondCountableTopology_iInf {α ι} [Countable ι] {t : ι → TopologicalSpace α}
    (ht : ∀ i, @SecondCountableTopology α (t i)) : @SecondCountableTopology α (⨅ i, t i) := by
  rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]
  exact SecondCountableTopology.mk' <|
    countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Second-Countability of Infimum of Countable Family of Second-Countable Topologies

Informal description

Let $\alpha$ be a type and $\iota$ be a countable type. Given a family of topologies $\{t_i\}_{i \in \iota}$ on $\alpha$ such that each $t_i$ is second-countable, the infimum topology $\bigsqcap_i t_i$ (i.e., the topology generated by the union of all open sets in each $t_i$) is also second-countable.

TopologicalSpace.instSecondCountableTopologyProd instance

 {β : Type*} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] :
  SecondCountableTopology (α × β)

Full source

instance {β : Type*} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] :
    SecondCountableTopology (α × β) :=
  ((isBasis_countableBasis α).prod (isBasis_countableBasis β)).secondCountableTopology <|
    (countable_countableBasis α).image2 (countable_countableBasis β) _

Product of Second-Countable Spaces is Second-Countable

Informal description

For any two topological spaces $\alpha$ and $\beta$ that are second-countable, their product space $\alpha \times \beta$ is also second-countable.

TopologicalSpace.instSecondCountableTopologyForallOfCountable instance

 {ι : Type*} {π : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (π a)] [∀ a, SecondCountableTopology (π a)] :
  SecondCountableTopology (∀ a, π a)

Full source

instance {ι : Type*} {π : ι → Type*} [Countable ι] [∀ a, TopologicalSpace (π a)]
    [∀ a, SecondCountableTopology (π a)] : SecondCountableTopology (∀ a, π a) :=
  secondCountableTopology_iInf fun _ => secondCountableTopology_induced _ _ _

Second-Countability of Countable Product of Second-Countable Spaces

Informal description

For any countable type $\iota$ and a family of topological spaces $\{\pi_a\}_{a \in \iota}$ where each $\pi_a$ is second-countable, the product space $\prod_{a \in \iota} \pi_a$ is also second-countable.

TopologicalSpace.SecondCountableTopology.to_separableSpace instance

[SecondCountableTopology α] : SeparableSpace α

Full source

instance (priority := 100) SecondCountableTopology.to_separableSpace [SecondCountableTopology α] :
    SeparableSpace α := by
  choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2
  exact ⟨⟨range p, countable_range _, (isBasis_countableBasis α).dense_iff.2 fun o ho _ =>
          ⟨p ⟨o, ho⟩, hp ⟨o, _⟩, mem_range_self _⟩⟩⟩

Second-Countable Spaces are Separable

Informal description

Every second-countable topological space is separable.

TopologicalSpace.secondCountableTopology_of_countable_cover theorem

 {ι} [Countable ι] {U : ι → Set α} [∀ i, SecondCountableTopology (U i)] (Uo : ∀ i, IsOpen (U i))
  (hc : ⋃ i, U i = univ) : SecondCountableTopology α

Full source

/-- A countable open cover induces a second-countable topology if all open covers
are themselves second countable. -/
theorem secondCountableTopology_of_countable_cover {ι} [Countable ι] {U : ι → Set α}
    [∀ i, SecondCountableTopology (U i)] (Uo : ∀ i, IsOpen (U i)) (hc : ⋃ i, U i = univ) :
    SecondCountableTopology α :=
  haveI : IsTopologicalBasis (⋃ i, image ((↑) : U i → α) '' countableBasis (U i)) :=
    isTopologicalBasis_of_cover Uo hc fun i => isBasis_countableBasis (U i)
  this.secondCountableTopology (countable_iUnion fun _ => (countable_countableBasis _).image _)

Second-Countability from Countable Open Cover of Second-Countable Subspaces

Informal description

Let $\alpha$ be a topological space with a countable open cover $\{U_i\}_{i \in \iota}$ (i.e., $\iota$ is countable and $\bigcup_i U_i = \alpha$). Suppose each $U_i$ is open and has a second-countable topology. Then $\alpha$ itself is second-countable.

TopologicalSpace.isOpen_iUnion_countable theorem

 [SecondCountableTopology α] {ι} (s : ι → Set α) (H : ∀ i, IsOpen (s i)) :
  ∃ T : Set ι, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i

Full source

/-- In a second-countable space, an open set, given as a union of open sets,
is equal to the union of countably many of those sets.
In particular, any open covering of `α` has a countable subcover: α is a Lindelöf space. -/
theorem isOpen_iUnion_countable [SecondCountableTopology α] {ι} (s : ι → Set α)
    (H : ∀ i, IsOpen (s i)) : ∃ T : Set ι, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i := by
  let B := { b ∈ countableBasis α | ∃ i, b ⊆ s i }
  choose f hf using fun b : B => b.2.2
  haveI : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype
  refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩
  rintro _ ⟨i, rfl⟩ x xs
  rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
  exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩

Countable Subcover Theorem for Second-Countable Spaces

Informal description

Let $\alpha$ be a second-countable topological space, and let $\{s_i\}_{i \in \iota}$ be a family of open sets in $\alpha$. Then there exists a countable subset $T \subseteq \iota$ such that the union of the sets $\{s_i\}_{i \in T}$ is equal to the union of all sets in the family, i.e., \[ \bigcup_{i \in T} s_i = \bigcup_{i \in \iota} s_i. \]

TopologicalSpace.isOpen_biUnion_countable theorem

 [SecondCountableTopology α] {ι : Type*} (I : Set ι) (s : ι → Set α) (H : ∀ i ∈ I, IsOpen (s i)) :
  ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Full source

theorem isOpen_biUnion_countable [SecondCountableTopology α] {ι : Type*} (I : Set ι) (s : ι → Set α)
    (H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i := by
  simp_rw [← Subtype.exists_set_subtype, biUnion_image]
  rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩
  exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

Countable Subcover Theorem for Indexed Families of Open Sets in Second-Countable Spaces

Informal description

Let $\alpha$ be a second-countable topological space, and let $\{s_i\}_{i \in I}$ be a family of open sets indexed by a subset $I$ of some type $\iota$. Then there exists a countable subset $T \subseteq I$ such that the union of the sets $\{s_i\}_{i \in T}$ is equal to the union of all sets in the family, i.e., \[ \bigcup_{i \in T} s_i = \bigcup_{i \in I} s_i. \]

TopologicalSpace.isOpen_sUnion_countable theorem

 [SecondCountableTopology α] (S : Set (Set α)) (H : ∀ s ∈ S, IsOpen s) :
  ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Full source

theorem isOpen_sUnion_countable [SecondCountableTopology α] (S : Set (Set α))
    (H : ∀ s ∈ S, IsOpen s) : ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S := by
  simpa only [and_left_comm, sUnion_eq_biUnion] using isOpen_biUnion_countable S id H

Countable Subcover Theorem for Union of Open Sets in Second-Countable Spaces

Informal description

Let $\alpha$ be a second-countable topological space, and let $S$ be a collection of open sets in $\alpha$. Then there exists a countable subcollection $T \subseteq S$ such that the union of all sets in $T$ equals the union of all sets in $S$, i.e., \[ \bigcup_{s \in T} s = \bigcup_{s \in S} s. \]

TopologicalSpace.countable_cover_nhds theorem

 [SecondCountableTopology α] {f : α → Set α} (hf : ∀ x, f x ∈ 𝓝 x) : ∃ s : Set α, s.Countable ∧ ⋃ x ∈ s, f x = univ

Full source

/-- In a topological space with second countable topology, if `f` is a function that sends each
point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
`x ∈ s`, cover the whole space. -/
theorem countable_cover_nhds [SecondCountableTopology α] {f : α → Set α} (hf : ∀ x, f x ∈ 𝓝 x) :
    ∃ s : Set α, s.Countable ∧ ⋃ x ∈ s, f x = univ := by
  rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
    ⟨s, hsc, hsU⟩
  suffices ⋃ x ∈ s, interior (f x) = univ from
    ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
  simp only [hsU, eq_univ_iff_forall, mem_iUnion]
  exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

Countable Neighborhood Cover Theorem for Second-Countable Spaces

Informal description

Let $\alpha$ be a second-countable topological space, and let $f : \alpha \to \text{Set } \alpha$ be a function such that for every $x \in \alpha$, $f(x)$ is a neighborhood of $x$. Then there exists a countable subset $s \subseteq \alpha$ such that the union of the neighborhoods $\bigcup_{x \in s} f(x)$ covers the entire space, i.e., $\bigcup_{x \in s} f(x) = \text{univ}$.

TopologicalSpace.countable_cover_nhdsWithin theorem

 [SecondCountableTopology α] {f : α → Set α} {s : Set α} (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) :
  ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Full source

theorem countable_cover_nhdsWithin [SecondCountableTopology α] {f : α → Set α} {s : Set α}
    (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x := by
  have : ∀ x : s, (↑) ⁻¹' f x(↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)
  rcases countable_cover_nhds this with ⟨t, htc, htU⟩
  refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩
  simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢
  exact htU ⟨x, hx⟩

Countable Neighborhood Cover Theorem for Subspaces of Second-Countable Spaces

Informal description

Let $\alpha$ be a second-countable topological space, $s \subseteq \alpha$ a subset, and $f : \alpha \to \text{Set } \alpha$ a function such that for every $x \in s$, $f(x)$ is a neighborhood of $x$ in the subspace topology of $s$. Then there exists a countable subset $t \subseteq s$ such that $s$ is covered by the union of the neighborhoods $\bigcup_{x \in t} f(x)$.

TopologicalSpace.IsTopologicalBasis.sigma theorem

 {s : ∀ i : ι, Set (Set (E i))} (hs : ∀ i, IsTopologicalBasis (s i)) :
  IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' s i)

Full source

/-- In a disjoint union space `Σ i, E i`, one can form a topological basis by taking the union of
topological bases on each of the parts of the space. -/
theorem IsTopologicalBasis.sigma {s : ∀ i : ι, Set (Set (E i))}
    (hs : ∀ i, IsTopologicalBasis (s i)) :
    IsTopologicalBasis (⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σi, E i))) '' s i) := by
  refine .of_hasBasis_nhds fun a ↦ ?_
  rw [Sigma.nhds_eq]
  convert (((hs a.1).nhds_hasBasis).map _).to_image_id
  aesop

Topological Basis for Disjoint Union via Component Bases

Informal description

Let $\{E_i\}_{i \in \iota}$ be a family of topological spaces indexed by $\iota$, and for each $i \in \iota$, let $s_i$ be a topological basis for $E_i$. Then the collection of all sets of the form $\Sigma.\text{mk}_i(u)$ for some $i \in \iota$ and $u \in s_i$ forms a topological basis for the disjoint union space $\Sigma i, E_i$.

TopologicalSpace.instSecondCountableTopologySigmaOfCountable instance

[Countable ι] [∀ i, SecondCountableTopology (E i)] : SecondCountableTopology (Σ i, E i)

Full source

/-- A countable disjoint union of second countable spaces is second countable. -/
instance [Countable ι] [∀ i, SecondCountableTopology (E i)] :
    SecondCountableTopology (Σi, E i) := by
  let b := ⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σi, E i))) '' countableBasis (E i)
  have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
  have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
  exact A.secondCountableTopology B

Second-Countability of Countable Disjoint Union of Second-Countable Spaces

Informal description

For any countable index type $\iota$ and a family of second-countable topological spaces $\{E_i\}_{i \in \iota}$, the disjoint union space $\Sigma i, E_i$ is also second-countable.

TopologicalSpace.IsTopologicalBasis.sum theorem

 {s : Set (Set α)} (hs : IsTopologicalBasis s) {t : Set (Set β)} (ht : IsTopologicalBasis t) :
  IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)

Full source

/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of
topological bases on each of the two components. -/
theorem IsTopologicalBasis.sum {s : Set (Set α)} (hs : IsTopologicalBasis s) {t : Set (Set β)}
    (ht : IsTopologicalBasis t) :
    IsTopologicalBasis ((fun u => Sum.inl '' u) '' s(fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t) := by
  apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
    · exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)
    · exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)
  · rintro (x | x) u hxu u_open
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
      exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩
    · obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2
      exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Topological Basis Construction for Sum Spaces

Informal description

Let $\alpha$ and $\beta$ be topological spaces with topological bases $s$ and $t$ respectively. Then the collection of sets formed by the union of the images of $s$ under the left inclusion map $\text{Sum.inl} : \alpha \to \alpha \oplus \beta$ and the images of $t$ under the right inclusion map $\text{Sum.inr} : \beta \to \alpha \oplus \beta$ is a topological basis for the sum space $\alpha \oplus \beta$. In other words, the set $\{\text{Sum.inl}(u) \mid u \in s\} \cup \{\text{Sum.inr}(v) \mid v \in t\}$ is a topological basis for $\alpha \oplus \beta$.

TopologicalSpace.instSecondCountableTopologySum instance

[SecondCountableTopology α] [SecondCountableTopology β] : SecondCountableTopology (α ⊕ β)

Full source

/-- A sum type of two second countable spaces is second countable. -/
instance [SecondCountableTopology α] [SecondCountableTopology β] :
    SecondCountableTopology (α ⊕ β) := by
  let b :=
    (fun u => Sum.inl '' u) '' countableBasis α(fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
  have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
  have B : b.Countable :=
    (Countable.image (countable_countableBasis _) _).union
      (Countable.image (countable_countableBasis _) _)
  exact A.secondCountableTopology B

Second-Countability of Sum Spaces

Informal description

The sum space $\alpha \oplus \beta$ of two second-countable topological spaces $\alpha$ and $\beta$ is also second-countable.

TopologicalSpace.IsTopologicalBasis.isQuotientMap theorem

 {V : Set (Set X)} (hV : IsTopologicalBasis V) (h' : IsQuotientMap π) (h : IsOpenMap π) :
  IsTopologicalBasis (Set.image π '' V)

Full source

/-- The image of a topological basis under an open quotient map is a topological basis. -/
theorem IsTopologicalBasis.isQuotientMap {V : Set (Set X)} (hV : IsTopologicalBasis V)
    (h' : IsQuotientMap π) (h : IsOpenMap π) : IsTopologicalBasis (Set.imageSet.image π '' V) := by
  apply isTopologicalBasis_of_isOpen_of_nhds
  · rintro - ⟨U, U_in_V, rfl⟩
    apply h U (hV.isOpen U_in_V)
  · intro y U y_in_U U_open
    obtain ⟨x, rfl⟩ := h'.surjective y
    let W := π ⁻¹' U
    have x_in_W : x ∈ W := y_in_U
    have W_open : IsOpen W := U_open.preimage h'.continuous
    obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
    have πZ_in_U : π '' Zπ '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)
    exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩

Image of Topological Basis Under Open Quotient Map is Basis

Informal description

Let $X$ and $Y$ be topological spaces, and let $\pi \colon X \to Y$ be an open quotient map. If $V$ is a topological basis for $X$, then the image $\pi(V) = \{\pi(U) \mid U \in V\}$ is a topological basis for $Y$.

Topology.IsQuotientMap.secondCountableTopology theorem

[SecondCountableTopology X] (h' : IsQuotientMap π) (h : IsOpenMap π) : SecondCountableTopology Y

Full source

/-- A second countable space is mapped by an open quotient map to a second countable space. -/
theorem _root_.Topology.IsQuotientMap.secondCountableTopology [SecondCountableTopology X]
    (h' : IsQuotientMap π) (h : IsOpenMap π) : SecondCountableTopology Y where
  is_open_generated_countable := by
    obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
    exact ⟨Set.image π '' V, V_countable.image (Set.image π),
      (V_generates.isQuotientMap h' h).eq_generateFrom⟩

Second-Countability Preserved Under Open Quotient Maps

Informal description

Let $X$ and $Y$ be topological spaces and $\pi \colon X \to Y$ be an open quotient map. If $X$ is second-countable, then $Y$ is also second-countable.

TopologicalSpace.IsTopologicalBasis.quotient theorem

 {V : Set (Set X)} (hV : IsTopologicalBasis V) (h : IsOpenMap (Quotient.mk' : X → Quotient S)) :
  IsTopologicalBasis (Set.image (Quotient.mk' : X → Quotient S) '' V)

Full source

/-- The image of a topological basis "downstairs" in an open quotient is a topological basis. -/
theorem IsTopologicalBasis.quotient {V : Set (Set X)} (hV : IsTopologicalBasis V)
    (h : IsOpenMap (Quotient.mk' : X → Quotient S)) :
    IsTopologicalBasis (Set.imageSet.image (Quotient.mk' : X → Quotient S) '' V) :=
  hV.isQuotientMap isQuotientMap_quotient_mk' h

Quotient Image of Topological Basis is Basis for Quotient Topology

Informal description

Let $X$ be a topological space with a topological basis $V$, and let $S$ be an equivalence relation on $X$. If the canonical projection $\pi \colon X \to X/S$ is an open map, then the image $\pi(V) = \{\pi(U) \mid U \in V\}$ forms a topological basis for the quotient space $X/S$.

TopologicalSpace.Quotient.secondCountableTopology theorem

[SecondCountableTopology X] (h : IsOpenMap (Quotient.mk' : X → Quotient S)) : SecondCountableTopology (Quotient S)

Full source

/-- An open quotient of a second countable space is second countable. -/
theorem Quotient.secondCountableTopology [SecondCountableTopology X]
    (h : IsOpenMap (Quotient.mk' : X → Quotient S)) : SecondCountableTopology (Quotient S) :=
  isQuotientMap_quotient_mk'.secondCountableTopology h

Second-Countability of Quotient Space under Open Projection

Informal description

Let $X$ be a second-countable topological space and let $S$ be an equivalence relation on $X$. If the canonical projection $\pi \colon X \to X/S$ is an open map, then the quotient space $X/S$ is also second-countable.

Topology.IsInducing.secondCountableTopology theorem

[TopologicalSpace β] [SecondCountableTopology β] (hf : IsInducing f) : SecondCountableTopology α

Full source

protected theorem Topology.IsInducing.secondCountableTopology [TopologicalSpace β]
    [SecondCountableTopology β] (hf : IsInducing f) : SecondCountableTopology α := by
  rw [hf.1]
  exact secondCountableTopology_induced α β f

Second-Countability of Induced Topology via Inducing Map

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ being second-countable. If $f : \alpha \to \beta$ is an inducing map (i.e., the topology on $\alpha$ is induced by $f$ from the topology on $\beta$), then $\alpha$ is also second-countable.

Topology.IsEmbedding.secondCountableTopology theorem

[TopologicalSpace β] [SecondCountableTopology β] (hf : IsEmbedding f) : SecondCountableTopology α

Full source

protected theorem Topology.IsEmbedding.secondCountableTopology
    [TopologicalSpace β] [SecondCountableTopology β]
    (hf : IsEmbedding f) : SecondCountableTopology α :=
  hf.1.secondCountableTopology

Second-Countability of Domain via Embedding into Second-Countable Space

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ being second-countable. If $f : \alpha \to \beta$ is an embedding (i.e., a homeomorphism onto its image), then $\alpha$ is also second-countable.

Topology.IsEmbedding.separableSpace theorem

 [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) : TopologicalSpace.SeparableSpace α

Full source

protected theorem Topology.IsEmbedding.separableSpace
    [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) :
    TopologicalSpace.SeparableSpace α := by
  have := hf.secondCountableTopology
  exact SecondCountableTopology.to_separableSpace

Separability of Domain via Embedding into Second-Countable Space

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ being second-countable. If $f : \alpha \to \beta$ is an embedding (i.e., a homeomorphism onto its image), then $\alpha$ is separable.

Mathlib.Topology.Bases

Main definitions

Main results

Implementation Notes

TODO