bases.lean

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro
-/
import topology.constructions
import topology.continuous_on

/-!
# Bases of topologies. Countability axioms.

A topological basis on a topological space `t` is a collection of sets,
such that all open sets can be generated as unions of these sets, without the need to take
finite intersections of them. This file introduces a framework for dealing with these collections,
and also what more we can say under certain countability conditions on bases,
which are referred to as first- and second-countable.
We also briefly cover the theory of separable spaces, which are those with a countable, dense
subset. If a space is second-countable, and also has a countably generated uniformity filter
(for example, if `t` is a metric space), it will automatically be separable (and indeed, these
conditions are equivalent in this case).

## Main definitions

* `topological_space.is_topological_basis s`: The topological space `t` has basis `s`.
* `topological_space.separable_space α`: The topological space `t` has a countable, dense subset.
* `topological_space.is_separable s`: The set `s` is contained in the closure of a countable set.
* `topological_space.first_countable_topology α`: A topology in which `𝓝 x` is countably generated
  for every `x`.
* `topological_space.second_countable_topology α`: A topology which has a topological basis which is
  countable.

## Main results

* `topological_space.first_countable_topology.tendsto_subseq`: In a first-countable space,
  cluster points are limits of subsequences.
* `topological_space.is_open_Union_countable`: In a second-countable space, the union of
  arbitrarily-many open sets is equal to a sub-union of only countably many of these sets.

## Implementation Notes
For our applications we are interested that there exists a countable basis, but we do not need the
concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.

### TODO:
More fine grained instances for `first_countable_topology`, `separable_space`, `t2_space`, and more
(see the comment below `subtype.second_countable_topology`.)
-/

open set filter function
open_locale topological_space filter
noncomputable theory

namespace topological_space

universe u
variables {α : Type u} [t : topological_space α]
include t

/-- 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 is_topological_basis (s : set (set α)) : Prop :=
(exists_subset_inter : ∀t₁∈s, ∀t₂∈s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃∈s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂)
(sUnion_eq : (⋃₀ s) = univ)
(eq_generate_from : t = generate_from s)

/-- If a family of sets `s` generates the topology, then nonempty intersections of finite
subcollections of `s` form a topological basis. -/
lemma is_topological_basis_of_subbasis {s : set (set α)} (hs : t = generate_from s) :
  is_topological_basis ((λ f, ⋂₀ f) '' {f : set (set α) | f.finite ∧ f ⊆ s ∧ (⋂₀ f).nonempty}) :=
begin
  refine ⟨_, _, _⟩,
  { rintro _ ⟨t₁, ⟨hft₁, ht₁b, ht₁⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b, ht₂⟩, rfl⟩ x h,
    have : ⋂₀ (t₁ ∪ t₂) = ⋂₀ t₁ ∩ ⋂₀ t₂ := sInter_union t₁ t₂,
    exact ⟨_, ⟨t₁ ∪ t₂, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b, this.symm ▸ ⟨x, h⟩⟩, this⟩, h,
      subset.rfl⟩ },
  { rw [sUnion_image, Union₂_eq_univ_iff],
    intro x, have : x ∈ ⋂₀ ∅, { rw sInter_empty, exact mem_univ x },
    exact ⟨∅, ⟨finite_empty, empty_subset _, x, this⟩, this⟩ },
  { rw hs,
    apply le_antisymm; apply le_generate_from,
    { rintro _ ⟨t, ⟨hft, htb, ht⟩, rfl⟩,
      exact @is_open_sInter _ (generate_from s) _ hft (λ s hs, generate_open.basic _ $ htb hs) },
    { intros t ht,
      rcases t.eq_empty_or_nonempty with rfl|hne, { apply @is_open_empty _ _ },
      rw ← sInter_singleton t at hne ⊢,
      exact generate_open.basic _ ⟨{t}, ⟨finite_singleton t, singleton_subset_iff.2 ht, hne⟩,
        rfl⟩ } }
end

/-- If a family of open sets `s` is such that every open neighbourhood contains some
member of `s`, then `s` is a topological basis. -/
lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
  (h_open : ∀ u ∈ s, is_open u)
  (h_nhds : ∀(a:α) (u : set α), a ∈ u → is_open u → ∃v ∈ s, a ∈ v ∧ v ⊆ u) :
  is_topological_basis s :=
begin
  refine ⟨λ t₁ ht₁ t₂ ht₂ x hx, h_nhds _ _ hx (is_open.inter (h_open _ ht₁) (h_open _ ht₂)), _, _⟩,
  { refine sUnion_eq_univ_iff.2 (λ a, _),
    rcases h_nhds a univ trivial is_open_univ with ⟨u, h₁, h₂, -⟩,
    exact ⟨u, h₁, h₂⟩ },
  { refine (le_generate_from h_open).antisymm (λ u hu, _),
    refine (@is_open_iff_nhds α (generate_from s) u).mpr (λ a ha, _),
    rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩,
    rw nhds_generate_from,
    exact infi₂_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu) }
end

/-- 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`. -/
lemma is_topological_basis.mem_nhds_iff {a : α} {s : set α} {b : set (set α)}
  (hb : is_topological_basis b) : s ∈ 𝓝 a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s :=
begin
  change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s,
  rw [hb.eq_generate_from, nhds_generate_from, binfi_sets_eq],
  { simp [and_assoc, and.left_comm] },
  { exact assume s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩,
      have a ∈ s ∩ t, from ⟨hs₁, ht₁⟩,
      let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ this in
      ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (subset.trans hu₃ (inter_subset_left _ _)),
        le_principal_iff.2 (subset.trans hu₃ (inter_subset_right _ _))⟩ },
  { rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩,
    exact ⟨i, h2, h1⟩ }
end

lemma is_topological_basis.is_open_iff {s : set α} {b : set (set α)} (hb : is_topological_basis b) :
  is_open s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s :=
by simp [is_open_iff_mem_nhds, hb.mem_nhds_iff]

lemma is_topological_basis.nhds_has_basis {b : set (set α)} (hb : is_topological_basis b) {a : α} :
  (𝓝 a).has_basis (λ t : set α, t ∈ b ∧ a ∈ t) (λ t, t) :=
⟨λ s, hb.mem_nhds_iff.trans $ by simp only [exists_prop, and_assoc]⟩

protected lemma is_topological_basis.is_open {s : set α} {b : set (set α)}
  (hb : is_topological_basis b) (hs : s ∈ b) : is_open s :=
by { rw hb.eq_generate_from, exact generate_open.basic s hs }

protected lemma is_topological_basis.mem_nhds {a : α} {s : set α} {b : set (set α)}
  (hb : is_topological_basis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ 𝓝 a :=
(hb.is_open hs).mem_nhds ha

lemma is_topological_basis.exists_subset_of_mem_open {b : set (set α)}
  (hb : is_topological_basis b) {a:α} {u : set α} (au : a ∈ u)
  (ou : is_open u) : ∃v ∈ b, a ∈ v ∧ v ⊆ u :=
hb.mem_nhds_iff.1 $ is_open.mem_nhds ou au

 /-- Any open set is the union of the basis sets contained in it. -/
lemma is_topological_basis.open_eq_sUnion' {B : set (set α)}
  (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
  u = ⋃₀ {s ∈ B | s ⊆ u} :=
ext $ λ a,
⟨λ ha, let ⟨b, hb, ab, bu⟩ := hB.exists_subset_of_mem_open ha ou in ⟨b, ⟨hb, bu⟩, ab⟩,
  λ ⟨b, ⟨hb, bu⟩, ab⟩, bu ab⟩

lemma is_topological_basis.open_eq_sUnion {B : set (set α)}
  (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
  ∃ S ⊆ B, u = ⋃₀ S :=
⟨{s ∈ B | s ⊆ u}, λ s h, h.1, hB.open_eq_sUnion' ou⟩

lemma is_topological_basis.open_eq_Union {B : set (set α)}
  (hB : is_topological_basis B) {u : set α} (ou : is_open u) :
  ∃ (β : Type u) (f : β → set α), u = (⋃ i, f i) ∧ ∀ i, f i ∈ B :=
⟨↥{s ∈ B | s ⊆ u}, coe, by { rw ← sUnion_eq_Union, apply hB.open_eq_sUnion' ou }, λ s, and.left s.2⟩

 /-- A point `a` is in the closure of `s` iff all basis sets containing `a` intersect `s`. -/
lemma is_topological_basis.mem_closure_iff {b : set (set α)} (hb : is_topological_basis b)
  {s : set α} {a : α} :
  a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).nonempty :=
(mem_closure_iff_nhds_basis' hb.nhds_has_basis).trans $ by simp only [and_imp]

 /-- A set is dense iff it has non-trivial intersection with all basis sets. -/
lemma is_topological_basis.dense_iff {b : set (set α)} (hb : is_topological_basis b) {s : set α} :
  dense s ↔ ∀ o ∈ b, set.nonempty o → (o ∩ s).nonempty :=
begin
  simp only [dense, hb.mem_closure_iff],
  exact ⟨λ h o hb ⟨a, ha⟩, h a o hb ha, λ h a o hb ha, h o hb ⟨a, ha⟩⟩
end

lemma is_topological_basis.is_open_map_iff {β} [topological_space β] {B : set (set α)}
  (hB : is_topological_basis B) {f : α → β} :
  is_open_map f ↔ ∀ s ∈ B, is_open (f '' s) :=
begin
  refine ⟨λ H o ho, H _ (hB.is_open ho), λ hf o ho, _⟩,
  rw [hB.open_eq_sUnion' ho, sUnion_eq_Union, image_Union],
  exact is_open_Union (λ s, hf s s.2.1)
end

lemma is_topological_basis.exists_nonempty_subset {B : set (set α)}
  (hb : is_topological_basis B) {u : set α} (hu : u.nonempty) (ou : is_open u) :
  ∃ v ∈ B, set.nonempty v ∧ v ⊆ u :=
begin
  cases hu with x hx,
  rw [hb.open_eq_sUnion' ou, mem_sUnion] at hx,
  rcases hx with ⟨v, hv, hxv⟩,
  exact ⟨v, hv.1, ⟨x, hxv⟩, hv.2⟩
end

lemma is_topological_basis_opens : is_topological_basis { U : set α | is_open U } :=
is_topological_basis_of_open_of_nhds (by tauto) (by tauto)

protected lemma is_topological_basis.prod {β} [topological_space β] {B₁ : set (set α)}
  {B₂ : set (set β)} (h₁ : is_topological_basis B₁) (h₂ : is_topological_basis B₂) :
  is_topological_basis (image2 (×ˢ) B₁ B₂) :=
begin
  refine is_topological_basis_of_open_of_nhds _ _,
  { rintro _ ⟨u₁, u₂, hu₁, hu₂, rfl⟩,
    exact (h₁.is_open hu₁).prod (h₂.is_open hu₂) },
  { rintro ⟨a, b⟩ u hu uo,
    rcases (h₁.nhds_has_basis.prod_nhds h₂.nhds_has_basis).mem_iff.1 (is_open.mem_nhds uo hu)
      with ⟨⟨s, t⟩, ⟨⟨hs, ha⟩, ht, hb⟩, hu⟩,
    exact ⟨s ×ˢ t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩ }
end

protected lemma is_topological_basis.inducing {β} [topological_space β]
  {f : α → β} {T : set (set β)} (hf : inducing f) (h : is_topological_basis T) :
  is_topological_basis (image (preimage f) T) :=
begin
  refine is_topological_basis_of_open_of_nhds _ _,
  { rintros _ ⟨V, hV, rfl⟩,
    rwa hf.is_open_iff,
    refine ⟨V, h.is_open hV, rfl⟩ },
  { intros a U ha hU,
    rw hf.is_open_iff at hU,
    obtain ⟨V, hV, rfl⟩ := hU,
    obtain ⟨S, hS, rfl⟩ := h.open_eq_sUnion hV,
    obtain ⟨W, hW, ha⟩ := ha,
    refine ⟨f ⁻¹' W, ⟨_, hS hW, rfl⟩, ha, set.preimage_mono $ set.subset_sUnion_of_mem hW⟩ }
end

lemma is_topological_basis_of_cover {ι} {U  : ι → set α} (Uo : ∀ i, is_open (U i))
  (Uc : (⋃ i, U i) = univ) {b : Π i, set (set (U i))} (hb : ∀ i, is_topological_basis (b i)) :
  is_topological_basis (⋃ i : ι, image (coe : U i → α) '' (b i)) :=
begin
  refine is_topological_basis_of_open_of_nhds (λ u hu, _) _,
  { simp only [mem_Union, mem_image] at hu,
    rcases hu with ⟨i, s, sb, rfl⟩,
    exact (Uo i).is_open_map_subtype_coe _ ((hb i).is_open sb) },
  { intros a u ha uo,
    rcases Union_eq_univ_iff.1 Uc a with ⟨i, hi⟩,
    lift a to ↥(U i) using hi,
    rcases (hb i).exists_subset_of_mem_open (by exact ha) (uo.preimage continuous_subtype_coe)
      with ⟨v, hvb, hav, hvu⟩,
    exact ⟨coe '' v, mem_Union.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
      image_subset_iff.2 hvu⟩ }
end

protected lemma is_topological_basis.continuous {β : Type*} [topological_space β]
  {B : set (set β)} (hB : is_topological_basis B) (f : α → β) (hf : ∀ s ∈ B, is_open (f ⁻¹' s)) :
  continuous f :=
begin rw hB.eq_generate_from, exact continuous_generated_from hf end

variables (α)

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

If `α` is a uniform space with countably generated uniformity filter (e.g., an `emetric_space`),
then this condition is equivalent to `topological_space.second_countable_topology α`. In this case
the latter should be used as a typeclass argument in theorems because Lean can automatically deduce
`separable_space` from `second_countable_topology` but it can't deduce `second_countable_topology`
and `emetric_space`. -/
class separable_space : Prop :=
(exists_countable_dense : ∃s:set α, countable s ∧ dense s)

lemma exists_countable_dense [separable_space α] :
  ∃ s : set α, countable s ∧ dense s :=
separable_space.exists_countable_dense

/-- 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 `topological_space.dense_seq` and
`topological_space.dense_range_dense_seq`.

If `α` might be empty, then `exists_countable_dense` is the main way to use separability of `α`. -/
lemma exists_dense_seq [separable_space α] [nonempty α] : ∃ u : ℕ → α, dense_range u :=
begin
  obtain ⟨s : set α, hs, s_dense⟩ := exists_countable_dense α,
  cases countable_iff_exists_surjective.mp hs with u hu,
  exact ⟨u, s_dense.mono hu⟩,
end

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

If `α` might be empty, then `exists_countable_dense` is the main way to use separability of `α`. -/
def dense_seq [separable_space α] [nonempty α] : ℕ → α := classical.some (exists_dense_seq α)

/-- The sequence `dense_seq α` has dense range. -/
@[simp] lemma dense_range_dense_seq [separable_space α] [nonempty α] :
  dense_range (dense_seq α) := classical.some_spec (exists_dense_seq α)

variable {α}

@[priority 100]
instance encodable.to_separable_space [encodable α] : separable_space α :=
{ exists_countable_dense := ⟨set.univ, set.countable_encodable set.univ, dense_univ⟩ }

lemma separable_space_of_dense_range {ι : Type*} [encodable ι] (u : ι → α) (hu : dense_range u) :
  separable_space α :=
⟨⟨range u, countable_range u, hu⟩⟩

/-- In a separable space, a family of nonempty disjoint open sets is countable. -/
lemma _root_.set.pairwise_disjoint.countable_of_is_open [separable_space α] {ι : Type*}
  {s : ι → set α} {a : set ι} (h : a.pairwise_disjoint s) (ha : ∀ i ∈ a, is_open (s i))
  (h'a : ∀ i ∈ a, (s i).nonempty) :
  countable a :=
begin
  rcases exists_countable_dense α with ⟨u, ⟨u_encodable⟩, u_dense⟩,
  have : ∀ i : a, ∃ y, y ∈ s i ∩ u :=
    λ i, dense_iff_inter_open.1 u_dense (s i) (ha i i.2) (h'a i i.2),
  choose f hfs hfu using this,
  lift f to a → u using hfu,
  have f_inj : injective f,
  { refine injective_iff_pairwise_ne.mpr ((h.subtype _ _).mono $ λ i j hij hfij, hij ⟨hfs i, _⟩),
    simp only [congr_arg coe hfij, hfs j] },
  exact ⟨@encodable.of_inj _ _ u_encodable f f_inj⟩
end

/-- In a separable space, a family of disjoint sets with nonempty interiors is countable. -/
lemma _root_.set.pairwise_disjoint.countable_of_nonempty_interior [separable_space α] {ι : Type*}
  {s : ι → set α} {a : set ι} (h : a.pairwise_disjoint s)
  (ha : ∀ i ∈ a, (interior (s i)).nonempty) :
  countable a :=
(h.mono $ λ i, interior_subset).countable_of_is_open (λ i hi, is_open_interior) ha

/-- 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 `separable_space s` or `is_separable (univ : set s))`. In metric spaces,
the two definitions are equivalent, see `topological_space.is_separable.separable_space`. -/
def is_separable (s : set α) :=
∃ c : set α, countable c ∧ s ⊆ closure c

lemma is_separable.mono {s u : set α} (hs : is_separable s) (hu : u ⊆ s) :
  is_separable u :=
begin
  rcases hs with ⟨c, c_count, hs⟩,
  exact ⟨c, c_count, hu.trans hs⟩
end

lemma is_separable.union {s u : set α} (hs : is_separable s) (hu : is_separable u) :
  is_separable (s ∪ u) :=
begin
  rcases hs with ⟨cs, cs_count, hcs⟩,
  rcases hu with ⟨cu, cu_count, hcu⟩,
  refine ⟨cs ∪ cu, cs_count.union cu_count, _⟩,
  exact union_subset (hcs.trans (closure_mono (subset_union_left _ _)))
    (hcu.trans (closure_mono (subset_union_right _ _)))
end

lemma is_separable.closure {s : set α} (hs : is_separable s) : is_separable (closure s) :=
begin
  rcases hs with ⟨c, c_count, hs⟩,
  exact ⟨c, c_count, by simpa using closure_mono hs⟩,
end

lemma is_separable_Union {ι : Type*} [encodable ι] {s : ι → set α} (hs : ∀ i, is_separable (s i)) :
  is_separable (⋃ i, s i) :=
begin
  choose c hc h'c using hs,
  refine ⟨⋃ i, c i, countable_Union hc, Union_subset_iff.2 (λ i, _)⟩,
  exact (h'c i).trans (closure_mono (subset_Union _ i))
end

lemma _root_.set.countable.is_separable {s : set α} (hs : countable s) : is_separable s :=
⟨s, hs, subset_closure⟩

lemma _root_.set.finite.is_separable {s : set α} (hs : s.finite) : is_separable s :=
hs.countable.is_separable

lemma is_separable_univ_iff :
  is_separable (univ : set α) ↔ separable_space α :=
begin
  split,
  { rintros ⟨c, c_count, hc⟩,
    refine ⟨⟨c, c_count, by rwa [dense_iff_closure_eq, ← univ_subset_iff]⟩⟩ },
  { introsI h,
    rcases exists_countable_dense α with ⟨c, c_count, hc⟩,
    exact ⟨c, c_count, by rwa [univ_subset_iff, ← dense_iff_closure_eq]⟩ }
end

lemma is_separable_of_separable_space [h : separable_space α] (s : set α) : is_separable s :=
is_separable.mono (is_separable_univ_iff.2 h) (subset_univ _)

lemma is_separable.image {β : Type*} [topological_space β]
  {s : set α} (hs : is_separable s) {f : α → β} (hf : continuous f) :
  is_separable (f '' s) :=
begin
  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)
end

lemma is_separable_of_separable_space_subtype (s : set α) [separable_space s] : is_separable s :=
begin
  have : is_separable ((coe : s → α) '' (univ : set s)) :=
    (is_separable_of_separable_space _).image continuous_subtype_coe,
  simpa only [image_univ, subtype.range_coe_subtype],
end

end topological_space

open topological_space

lemma is_topological_basis_pi {ι : Type*} {X : ι → Type*}
  [∀ i, topological_space (X i)] {T : Π i, set (set (X i))}
  (cond : ∀ i, is_topological_basis (T i)) :
  is_topological_basis {S : set (Π i, X i) | ∃ (U : Π i, set (X i)) (F : finset ι),
    (∀ i, i ∈ F → (U i) ∈ T i) ∧ S = (F : set ι).pi U } :=
begin
  refine is_topological_basis_of_open_of_nhds _ _,
  { rintro _ ⟨U, F, h1, rfl⟩,
    apply is_open_set_pi F.finite_to_set,
    intros i hi,
    exact (cond i).is_open (h1 i hi) },
  { intros a U ha hU,
    obtain ⟨I, t, hta, htU⟩ :
      ∃ (I : finset ι) (t : Π (i : ι), set (X i)), (∀ i, t i ∈ 𝓝 (a i)) ∧ set.pi ↑I t ⊆ U,
    { rw [← filter.mem_pi', ← nhds_pi], exact hU.mem_nhds ha },
    have : ∀ i, ∃ V ∈ T i, a i ∈ V ∧ V ⊆ t i := λ i, (cond i).mem_nhds_iff.1 (hta i),
    choose V hVT haV hVt,
    exact ⟨_, ⟨V, I, λ i hi, hVT i, rfl⟩, λ i hi, haV i, (pi_mono $ λ i hi, hVt i).trans htU⟩ },
end

lemma is_topological_basis_infi {β : Type*} {ι : Type*} {X : ι → Type*}
  [t : ∀ i, topological_space (X i)] {T : Π i, set (set (X i))}
  (cond : ∀ i, is_topological_basis (T i)) (f : Π i, β → X i) :
  @is_topological_basis β (⨅ i, induced (f i) (t i))
  { S | ∃ (U : Π i, set (X i)) (F : finset ι),
    (∀ i, i ∈ F → U i ∈ T i) ∧ S = ⋂ i (hi : i ∈ F), (f i) ⁻¹' (U i) } :=
begin
  convert (is_topological_basis_pi cond).inducing (inducing_infi_to_pi _),
  ext V,
  split,
  { rintros ⟨U, F, h1, h2⟩,
    have : (F : set ι).pi U = (⋂ (i : ι) (hi : i ∈ F),
        (λ (z : Π j, X j), z i) ⁻¹' (U i)), by { ext, simp },
    refine ⟨(F : set ι).pi U, ⟨U, F, h1, rfl⟩, _⟩,
    rw [this, h2, set.preimage_Inter],
    congr' 1,
    ext1,
    rw set.preimage_Inter,
    refl },
  { rintros ⟨U, ⟨U, F, h1, rfl⟩, h⟩,
    refine ⟨U, F, h1, _⟩,
    have : (F : set ι).pi U = (⋂ (i : ι) (hi : i ∈ F),
        (λ (z : Π j, X j), z i) ⁻¹' (U i)), by { ext, simp },
    rw [← h, this, set.preimage_Inter],
    congr' 1,
    ext1,
    rw set.preimage_Inter,
    refl }
end

lemma is_topological_basis_singletons (α : Type*) [topological_space α] [discrete_topology α] :
  is_topological_basis {s | ∃ (x : α), (s : set α) = {x}} :=
is_topological_basis_of_open_of_nhds (λ u hu, is_open_discrete _) $
  λ x u hx u_open, ⟨{x}, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩

/-- 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 lemma dense_range.separable_space {α β : Type*} [topological_space α] [separable_space α]
  [topological_space β] {f : α → β} (h : dense_range f) (h' : continuous f) :
  separable_space β :=
let ⟨s, s_cnt, s_dense⟩ := exists_countable_dense α in
⟨⟨f '' s, countable.image s_cnt f, h.dense_image h' s_dense⟩⟩

lemma dense.exists_countable_dense_subset {α : Type*} [topological_space α]
  {s : set α} [separable_space s] (hs : dense s) :
  ∃ t ⊆ s, countable t ∧ dense t :=
let ⟨t, htc, htd⟩ := exists_countable_dense s
in ⟨coe '' t, image_subset_iff.2 $ λ x _, mem_preimage.2 $ subtype.coe_prop _, htc.image coe,
  hs.dense_range_coe.dense_image continuous_subtype_val htd⟩

/-- 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`. -/
lemma dense.exists_countable_dense_subset_bot_top {α : Type*} [topological_space α]
  [partial_order α] {s : set α} [separable_space s] (hs : dense s) :
  ∃ t ⊆ s, countable t ∧ dense t ∧ (∀ x, is_bot x → x ∈ s → x ∈ t) ∧
    (∀ x, is_top x → x ∈ s → x ∈ t) :=
begin
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩,
  refine ⟨(t ∪ ({x | is_bot x} ∪ {x | is_top x})) ∩ s, _, _, _, _, _⟩,
  exacts [inter_subset_right _ _,
    (htc.union ((countable_is_bot α).union (countable_is_top α))).mono (inter_subset_left _ _),
    htd.mono (subset_inter (subset_union_left _ _) hts),
    λ x hx hxs, ⟨or.inr $ or.inl hx, hxs⟩, λ x hx hxs, ⟨or.inr $ or.inr hx, hxs⟩]
end

instance separable_space_univ {α : Type*} [topological_space α] [separable_space α] :
  separable_space (univ : set α) :=
(equiv.set.univ α).symm.surjective.dense_range.separable_space
  (continuous_subtype_mk _ continuous_id)

/-- 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`. -/
lemma exists_countable_dense_bot_top (α : Type*) [topological_space α] [separable_space α]
  [partial_order α] :
  ∃ s : set α, countable s ∧ dense s ∧ (∀ x, is_bot x → x ∈ s) ∧ (∀ x, is_top x → x ∈ s) :=
by simpa using dense_univ.exists_countable_dense_subset_bot_top

namespace topological_space
universe u
variables (α : Type u) [t : topological_space α]
include t


/-- A first-countable space is one in which every point has a
  countable neighborhood basis. -/
class first_countable_topology : Prop :=
(nhds_generated_countable : ∀a:α, (𝓝 a).is_countably_generated)

attribute [instance] first_countable_topology.nhds_generated_countable

namespace first_countable_topology
variable {α}

/-- In a first-countable space, a cluster point `x` of a sequence
is the limit of some subsequence. -/
lemma tendsto_subseq [first_countable_topology α] {u : ℕ → α} {x : α}
  (hx : map_cluster_pt x at_top u) :
  ∃ (ψ : ℕ → ℕ), (strict_mono ψ) ∧ (tendsto (u ∘ ψ) at_top (𝓝 x)) :=
subseq_tendsto_of_ne_bot hx

end first_countable_topology

variables {α}

instance is_countably_generated_nhds_within (x : α) [is_countably_generated (𝓝 x)] (s : set α) :
  is_countably_generated (𝓝[s] x) :=
inf.is_countably_generated _ _

variable (α)

/-- A second-countable space is one with a countable basis. -/
class second_countable_topology : Prop :=
(is_open_generated_countable [] :
  ∃ b : set (set α), countable b ∧ t = topological_space.generate_from b)

variable {α}

protected lemma is_topological_basis.second_countable_topology
  {b : set (set α)} (hb : is_topological_basis b) (hc : countable b) :
  second_countable_topology α :=
⟨⟨b, hc, hb.eq_generate_from⟩⟩

variable (α)

lemma exists_countable_basis [second_countable_topology α] :
  ∃b:set (set α), countable b ∧ ∅ ∉ b ∧ is_topological_basis b :=
let ⟨b, hb₁, hb₂⟩ := second_countable_topology.is_open_generated_countable α in
let b' := (λs, ⋂₀ s) '' {s:set (set α) | s.finite ∧ s ⊆ b ∧ (⋂₀ s).nonempty} in
⟨b',
  ((countable_set_of_finite_subset hb₁).mono
    (by { simp only [← and_assoc], apply inter_subset_left })).image _,
  assume ⟨s, ⟨_, _, hn⟩, hp⟩, absurd hn (not_nonempty_iff_eq_empty.2 hp),
  is_topological_basis_of_subbasis hb₂⟩

/-- A countable topological basis of `α`. -/
def countable_basis [second_countable_topology α] : set (set α) :=
(exists_countable_basis α).some

lemma countable_countable_basis [second_countable_topology α] : countable (countable_basis α) :=
(exists_countable_basis α).some_spec.1

instance encodable_countable_basis [second_countable_topology α] :
  encodable (countable_basis α) :=
(countable_countable_basis α).to_encodable

lemma empty_nmem_countable_basis [second_countable_topology α] : ∅ ∉ countable_basis α :=
(exists_countable_basis α).some_spec.2.1

lemma is_basis_countable_basis [second_countable_topology α] :
  is_topological_basis (countable_basis α) :=
(exists_countable_basis α).some_spec.2.2

lemma eq_generate_from_countable_basis [second_countable_topology α] :
  ‹topological_space α› = generate_from (countable_basis α) :=
(is_basis_countable_basis α).eq_generate_from

variable {α}

lemma is_open_of_mem_countable_basis [second_countable_topology α] {s : set α}
  (hs : s ∈ countable_basis α) : is_open s :=
(is_basis_countable_basis α).is_open hs

lemma nonempty_of_mem_countable_basis [second_countable_topology α] {s : set α}
  (hs : s ∈ countable_basis α) : s.nonempty :=
ne_empty_iff_nonempty.1 $ ne_of_mem_of_not_mem hs $ empty_nmem_countable_basis α

variable (α)

@[priority 100] -- see Note [lower instance priority]
instance second_countable_topology.to_first_countable_topology
  [second_countable_topology α] : first_countable_topology α :=
⟨λ x, has_countable_basis.is_countably_generated $
  ⟨(is_basis_countable_basis α).nhds_has_basis, (countable_countable_basis α).mono $
    inter_subset_left _ _⟩⟩

/-- If `β` is a second-countable space, then its induced topology
via `f` on `α` is also second-countable. -/
lemma second_countable_topology_induced (β)
  [t : topological_space β] [second_countable_topology β] (f : α → β) :
  @second_countable_topology α (t.induced f) :=
begin
  rcases second_countable_topology.is_open_generated_countable β with ⟨b, hb, eq⟩,
  refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, _⟩ },
  rw [eq, induced_generate_from_eq]
end

instance subtype.second_countable_topology (s : set α) [second_countable_topology α] :
  second_countable_topology s :=
second_countable_topology_induced s α coe

/- TODO: more fine grained instances for first_countable_topology, separable_space, t2_space, ... -/
instance {β : Type*} [topological_space β]
  [second_countable_topology α] [second_countable_topology β] : second_countable_topology (α × β) :=
((is_basis_countable_basis α).prod (is_basis_countable_basis β)).second_countable_topology $
  (countable_countable_basis α).image2 (countable_countable_basis β) _

instance second_countable_topology_encodable {ι : Type*} {π : ι → Type*}
  [encodable ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
  second_countable_topology (∀a, π a) :=
begin
  have : t = (λa, generate_from (countable_basis (π a))),
    from funext (assume a, (is_basis_countable_basis (π a)).eq_generate_from),
  rw [this, pi_generate_from_eq],
  constructor, refine ⟨_, _, rfl⟩,
  have : countable {T : set (Π i, π i) | ∃ (I : finset ι) (s : Π i : I, set (π i)),
    (∀ i, s i ∈ countable_basis (π i)) ∧ T = {f | ∀ i : I, f i ∈ s i}},
  { simp only [set_of_exists, ← exists_prop],
    refine countable_Union (λ I, countable.bUnion _ (λ _ _, countable_singleton _)),
    change countable {s : Π i : I, set (π i) | ∀ i, s i ∈ countable_basis (π i)},
    exact countable_pi (λ i, countable_countable_basis _) },
  convert this using 1, ext1 T, split,
  { rintro ⟨s, I, hs, rfl⟩,
    refine ⟨I, λ i, s i, λ i, hs i i.2, _⟩,
    simp only [set.pi, set_coe.forall'], refl },
  { rintro ⟨I, s, hs, rfl⟩,
    rcases @subtype.surjective_restrict ι (λ i, set (π i)) _ (λ i, i ∈ I) s with ⟨s, rfl⟩,
    exact ⟨s, I, λ i hi, hs ⟨i, hi⟩, set.ext $ λ f, subtype.forall⟩ }
end

instance second_countable_topology_fintype {ι : Type*} {π : ι → Type*}
  [fintype ι] [t : ∀a, topological_space (π a)] [∀a, second_countable_topology (π a)] :
  second_countable_topology (∀a, π a) :=
by { letI := fintype.to_encodable ι, exact topological_space.second_countable_topology_encodable }

@[priority 100] -- see Note [lower instance priority]
instance second_countable_topology.to_separable_space
  [second_countable_topology α] : separable_space α :=
begin
  choose p hp using λ s : countable_basis α, nonempty_of_mem_countable_basis s.2,
  exact ⟨⟨range p, countable_range _,
    (is_basis_countable_basis α).dense_iff.2 $ λ o ho _, ⟨p ⟨o, ho⟩, hp _, mem_range_self _⟩⟩⟩
end

variables {α}

/-- A countable open cover induces a second-countable topology if all open covers
are themselves second countable. -/
lemma second_countable_topology_of_countable_cover {ι} [encodable ι] {U : ι → set α}
  [∀ i, second_countable_topology (U i)] (Uo : ∀ i, is_open (U i))  (hc : (⋃ i, U i) = univ) :
  second_countable_topology α :=
begin
  have : is_topological_basis (⋃ i, image (coe : U i → α) '' (countable_basis (U i))),
    from is_topological_basis_of_cover Uo hc (λ i, is_basis_countable_basis (U i)),
  exact this.second_countable_topology
    (countable_Union $ λ i, (countable_countable_basis _).image _)
end

section sigma

variables {ι : Type*} {E : ι → Type*} [∀ i, topological_space (E i)]
omit t

/-- 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. -/
lemma is_topological_basis.sigma
  {s : Π (i : ι), set (set (E i))} (hs : ∀ i, is_topological_basis (s i)) :
  is_topological_basis (⋃ (i : ι), (λ u, ((sigma.mk i) '' u : set (Σ i, E i))) '' (s i)) :=
begin
  apply is_topological_basis_of_open_of_nhds,
  { assume u hu,
    obtain ⟨i, t, ts, rfl⟩ : ∃ (i : ι) (t : set (E i)), t ∈ s i ∧ sigma.mk i '' t = u,
      by simpa only [mem_Union, mem_image] using hu,
    exact is_open_map_sigma_mk _ ((hs i).is_open ts) },
  { rintros ⟨i, x⟩ u hxu u_open,
    have hx : x ∈ sigma.mk i ⁻¹' u := hxu,
    obtain ⟨v, vs, xv, hv⟩ : ∃ (v : set (E i)) (H : v ∈ s i), x ∈ v ∧ v ⊆ sigma.mk i ⁻¹' u :=
      (hs i).exists_subset_of_mem_open hx (is_open_sigma_iff.1 u_open i),
    exact ⟨(sigma.mk i) '' v, mem_Union.2 ⟨i, mem_image_of_mem _ vs⟩, mem_image_of_mem _ xv,
      image_subset_iff.2 hv⟩ }
end

/-- A countable disjoint union of second countable spaces is second countable. -/
instance [encodable ι] [∀ i, second_countable_topology (E i)] :
  second_countable_topology (Σ i, E i) :=
begin
  let b := (⋃ (i : ι), (λ u, ((sigma.mk i) '' u : set (Σ i, E i))) '' (countable_basis (E i))),
  have A : is_topological_basis b := is_topological_basis.sigma (λ i, is_basis_countable_basis  _),
  have B : countable b := countable_Union (λ i, countable.image (countable_countable_basis _) _),
  exact A.second_countable_topology B,
end

end sigma


section sum
omit t

variables {β : Type*} [topological_space α] [topological_space β]

/-- In a sum space `α ⊕ β`, one can form a topological basis by taking the union of
topological bases on each of the two components. -/
lemma is_topological_basis.sum
  {s : set (set α)} (hs : is_topological_basis s) {t : set (set β)} (ht : is_topological_basis t) :
  is_topological_basis (((λ u, sum.inl '' u) '' s) ∪ ((λ u, sum.inr '' u) '' t)) :=
begin
  apply is_topological_basis_of_open_of_nhds,
  { assume u hu,
    cases hu,
    { rcases hu with ⟨w, hw, rfl⟩,
      exact open_embedding_inl.is_open_map w (hs.is_open hw) },
    { rcases hu with ⟨w, hw, rfl⟩,
      exact open_embedding_inr.is_open_map w (ht.is_open hw) } },
  { rintros x u hxu u_open,
    cases x,
    { have h'x : x ∈ sum.inl ⁻¹' u := hxu,
      obtain ⟨v, vs, xv, vu⟩ : ∃ (v : set α) (H : v ∈ s), x ∈ v ∧ v ⊆ sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open h'x (is_open_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⟩ },
    { have h'x : x ∈ sum.inr ⁻¹' u := hxu,
      obtain ⟨v, vs, xv, vu⟩ : ∃ (v : set β) (H : v ∈ t), x ∈ v ∧ v ⊆ sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open h'x (is_open_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⟩ } }
end

/-- A sum type of two second countable spaces is second countable. -/
instance [second_countable_topology α] [second_countable_topology β] :
  second_countable_topology (α ⊕ β) :=
begin
  let b := (λ u, sum.inl '' u) '' (countable_basis α) ∪ (λ u, sum.inr '' u) '' (countable_basis β),
  have A : is_topological_basis b := (is_basis_countable_basis α).sum (is_basis_countable_basis β),
  have B : countable b := (countable.image (countable_countable_basis _) _).union
    (countable.image (countable_countable_basis _) _),
  exact A.second_countable_topology B,
end

end sum

end topological_space

open topological_space

variables {α β : Type*} [topological_space α] [topological_space β] {f : α → β}

protected lemma inducing.second_countable_topology [second_countable_topology β]
  (hf : inducing f) : second_countable_topology α :=
by { rw hf.1, exact second_countable_topology_induced α β f }

protected lemma embedding.second_countable_topology [second_countable_topology β]
  (hf : embedding f) : second_countable_topology α :=
hf.1.second_countable_topology