[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsTopologicalBasis (insert ∅ s)
[PROOFSTEP]
refine' ⟨_, by rw [sUnion_insert, empty_union, h.sUnion_eq], _⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ⋃₀ insert ∅ s = univ
[PROOFSTEP]
rw [sUnion_insert, empty_union, h.sUnion_eq]
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ (t₁ : Set α),
    t₁ ∈ insert ∅ s →
      ∀ (t₂ : Set α), t₂ ∈ insert ∅ s → ∀ (x : α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro t₁ (rfl | h₁) t₂ (rfl | h₂) x ⟨hx₁, hx₂⟩
[GOAL]
case refine'_1.inl.inl.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
x : α
hx₁ hx₂ : x ∈ ∅
⊢ ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ ∅ ∩ ∅
[PROOFSTEP]
cases hx₁
[GOAL]
case refine'_1.inl.inr.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx₁ : x ∈ ∅
hx₂ : x ∈ t₂
⊢ ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ ∅ ∩ t₂
[PROOFSTEP]
cases hx₁
[GOAL]
case refine'_1.inr.inl.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
x : α
hx₁ : x ∈ t₁
hx₂ : x ∈ ∅
⊢ ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ ∅
[PROOFSTEP]
cases hx₂
[GOAL]
case refine'_1.inr.inr.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx₁ : x ∈ t₁
hx₂ : x ∈ t₂
⊢ ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
obtain ⟨t₃, h₃, hs⟩ := h.exists_subset_inter _ h₁ _ h₂ x ⟨hx₁, hx₂⟩
[GOAL]
case refine'_1.inr.inr.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx₁ : x ∈ t₁
hx₂ : x ∈ t₂
t₃ : Set α
h₃ : t₃ ∈ s
hs : x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ ∃ t₃, t₃ ∈ insert ∅ s ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
exact ⟨t₃, .inr h₃, hs⟩
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ t = generateFrom (insert ∅ s)
[PROOFSTEP]
rw [h.eq_generateFrom]
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ generateFrom s = generateFrom (insert ∅ s)
[PROOFSTEP]
refine' le_antisymm (le_generateFrom fun t => _) (generateFrom_anti <| subset_insert ∅ s)
[GOAL]
case refine'_2
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
⊢ t ∈ insert ∅ s → IsOpen t
[PROOFSTEP]
rintro (rfl | ht)
[GOAL]
case refine'_2.inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsOpen ∅
[PROOFSTEP]
exact @isOpen_empty _ (generateFrom s)
[GOAL]
case refine'_2.inr
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
⊢ IsOpen t
[PROOFSTEP]
exact .basic t ht
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsTopologicalBasis (s \ {∅})
[PROOFSTEP]
refine' ⟨_, by rw [sUnion_diff_singleton_empty, h.sUnion_eq], _⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ⋃₀ (s \ {∅}) = univ
[PROOFSTEP]
rw [sUnion_diff_singleton_empty, h.sUnion_eq]
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ (t₁ : Set α),
    t₁ ∈ s \ {∅} → ∀ (t₂ : Set α), t₂ ∈ s \ {∅} → ∀ (x : α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ s \ {∅} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro t₁ ⟨h₁, -⟩ t₂ ⟨h₂, -⟩ x hx
[GOAL]
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃, t₃ ∈ s \ {∅} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
obtain ⟨t₃, h₃, hs⟩ := h.exists_subset_inter _ h₁ _ h₂ x hx
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
t₃ : Set α
h₃ : t₃ ∈ s
hs : x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ ∃ t₃, t₃ ∈ s \ {∅} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
exact ⟨t₃, ⟨h₃, Nonempty.ne_empty ⟨x, hs.1⟩⟩, hs⟩
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ t = generateFrom (s \ {∅})
[PROOFSTEP]
rw [h.eq_generateFrom]
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ generateFrom s = generateFrom (s \ {∅})
[PROOFSTEP]
refine' le_antisymm (generateFrom_anti <| diff_subset s _) (le_generateFrom fun t ht => _)
[GOAL]
case refine'_2
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
⊢ IsOpen t
[PROOFSTEP]
obtain rfl | he := eq_or_ne t ∅
[GOAL]
case refine'_2.inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
ht : ∅ ∈ s
⊢ IsOpen ∅
[PROOFSTEP]
exact @isOpen_empty _ (generateFrom _)
[GOAL]
case refine'_2.inr
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
he : t ≠ ∅
⊢ IsOpen t
[PROOFSTEP]
exact .basic t ⟨ht, he⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hs : t = generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
[PROOFSTEP]
subst t
[GOAL]
α : Type u
s : Set (Set α)
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
[PROOFSTEP]
letI := generateFrom s
[GOAL]
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ IsTopologicalBasis ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s})
[PROOFSTEP]
refine' ⟨_, _, le_antisymm (le_generateFrom _) <| generateFrom_anti fun t ht => _⟩
[GOAL]
case refine'_1
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (t₁ : Set α),
    t₁ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
      ∀ (t₂ : Set α),
        t₂ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} →
          ∀ (x : α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro _ ⟨t₁, ⟨hft₁, ht₁b⟩, rfl⟩ _ ⟨t₂, ⟨hft₂, ht₂b⟩, rfl⟩ x h
[GOAL]
case refine'_1.intro.intro.intro.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t₁ : Set (Set α)
hft₁ : Set.Finite t₁
ht₁b : t₁ ⊆ s
t₂ : Set (Set α)
hft₂ : Set.Finite t₂
ht₂b : t₂ ⊆ s
x : α
h : x ∈ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
⊢ ∃ t₃, t₃ ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} ∧ x ∈ t₃ ∧ t₃ ⊆ (fun f => ⋂₀ f) t₁ ∩ (fun f => ⋂₀ f) t₂
[PROOFSTEP]
exact ⟨_, ⟨_, ⟨hft₁.union hft₂, union_subset ht₁b ht₂b⟩, sInter_union t₁ t₂⟩, h, Subset.rfl⟩
[GOAL]
case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃₀ ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}) = univ
[PROOFSTEP]
rw [sUnion_image, iUnion₂_eq_univ_iff]
[GOAL]
case refine'_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i j, a ∈ ⋂₀ i
[PROOFSTEP]
exact fun x => ⟨∅, ⟨finite_empty, empty_subset _⟩, sInter_empty.substr <| mem_univ x⟩
[GOAL]
case refine'_3
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (s_1 : Set α), s_1 ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s} → IsOpen s_1
[PROOFSTEP]
rintro _ ⟨t, ⟨hft, htb⟩, rfl⟩
[GOAL]
case refine'_3.intro.intro.intro
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ IsOpen ((fun f => ⋂₀ f) t)
[PROOFSTEP]
apply isOpen_sInter
[GOAL]
case refine'_3.intro.intro.intro.hs
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ Set.Finite t
case refine'_3.intro.intro.intro.a
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set (Set α)
hft : Set.Finite t
htb : t ⊆ s
⊢ ∀ (t_1 : Set α), t_1 ∈ t → IsOpen t_1
[PROOFSTEP]
exacts [hft, fun s hs => GenerateOpen.basic _ <| htb hs]
[GOAL]
case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ t ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
[PROOFSTEP]
rw [← sInter_singleton t]
[GOAL]
case refine'_4
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
t : Set α
ht : t ∈ s
⊢ ⋂₀ {t} ∈ (fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ s}
[PROOFSTEP]
exact ⟨{ t }, ⟨finite_singleton t, singleton_subset_iff.2 ht⟩, rfl⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis s
[PROOFSTEP]
refine' ⟨fun t₁ ht₁ t₂ ht₂ x hx => h_nhds _ _ hx (IsOpen.inter (h_open _ ht₁) (h_open _ ht₂)), _, _⟩
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ ⋃₀ s = univ
[PROOFSTEP]
refine' sUnion_eq_univ_iff.2 fun a => _
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
⊢ ∃ b, b ∈ s ∧ a ∈ b
[PROOFSTEP]
rcases h_nhds a univ trivial isOpen_univ with ⟨u, h₁, h₂, -⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
a : α
u : Set α
h₁ : u ∈ s
h₂ : a ∈ u
⊢ ∃ b, b ∈ s ∧ a ∈ b
[PROOFSTEP]
exact ⟨u, h₁, h₂⟩
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
⊢ t = generateFrom s
[PROOFSTEP]
refine' (le_generateFrom h_open).antisymm fun u hu => _
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
⊢ IsOpen u
[PROOFSTEP]
refine' (@isOpen_iff_nhds α (generateFrom s) u).mpr fun a ha => _
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
⊢ 𝓝 a ≤ 𝓟 u
[PROOFSTEP]
rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ 𝓝 a ≤ 𝓟 u
[PROOFSTEP]
rw [nhds_generateFrom]
[GOAL]
case refine'_2.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_open : ∀ (u : Set α), u ∈ s → IsOpen u
h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ s ∧ a ∈ v ∧ v ⊆ u
u : Set α
hu : IsOpen u
a : α
ha : a ∈ u
v : Set α
hvs : v ∈ s
hav : a ∈ v
hvu : v ⊆ u
⊢ ⨅ (s_1 : Set α) (_ : s_1 ∈ {s_2 | a ∈ s_2 ∧ s_2 ∈ s}), 𝓟 s_1 ≤ 𝓟 u
[PROOFSTEP]
exact iInf₂_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu)
[GOAL]
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ 𝓝 a ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
[PROOFSTEP]
change s ∈ (𝓝 a).sets ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s
[GOAL]
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ (𝓝 a).sets ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
[PROOFSTEP]
rw [hb.eq_generateFrom, nhds_generateFrom, biInf_sets_eq]
[GOAL]
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ s ∈ ⋃ (i : Set α) (_ : i ∈ {s | a ∈ s ∧ s ∈ b}), (𝓟 i).sets ↔ ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
[PROOFSTEP]
simp [and_assoc, and_left_comm]
[GOAL]
case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) {s | a ∈ s ∧ s ∈ b}
[PROOFSTEP]
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
[GOAL]
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
[PROOFSTEP]
let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
[GOAL]
case h.intro.intro
α : Type u
t✝ : TopologicalSpace α
a : α
s✝ : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
hs₁ : a ∈ s
hs₂ : s ∈ b
t : Set α
ht₁ : a ∈ t
ht₂ : t ∈ b
u : Set α
hu₁ : u ∈ b
hu₂ : a ∈ u
hu₃ : u ⊆ s ∩ t
⊢ ∃ z,
    z ∈ {s | a ∈ s ∧ s ∈ b} ∧
      ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) s z ∧ ((fun s => 𝓟 s) ⁻¹'o fun x x_1 => x ≥ x_1) t z
[PROOFSTEP]
exact
  ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans (inter_subset_left _ _)),
    le_principal_iff.2 (hu₃.trans (inter_subset_right _ _))⟩
[GOAL]
case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
[PROOFSTEP]
rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
[GOAL]
case ne.intro.intro
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
i : Set α
h1 : i ∈ b
h2 : a ∈ i
⊢ Set.Nonempty {s | a ∈ s ∧ s ∈ b}
[PROOFSTEP]
exact ⟨i, h2, h1⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ IsOpen s ↔ ∀ (a : α), a ∈ s → ∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s
[PROOFSTEP]
simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]
[GOAL]
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
a : α
s : Set α
⊢ (∃ t, t ∈ b ∧ a ∈ t ∧ t ⊆ s) ↔ ∃ i, (i ∈ b ∧ a ∈ i) ∧ i ⊆ s
[PROOFSTEP]
simp only [and_assoc]
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen s
[PROOFSTEP]
rw [hb.eq_generateFrom]
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen s
[PROOFSTEP]
exact .basic s hs
[GOAL]
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃ (i : ↑{s | s ∈ B ∧ s ⊆ u}), ↑i
[PROOFSTEP]
rw [← sUnion_eq_iUnion]
[GOAL]
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
[PROOFSTEP]
apply hB.open_eq_sUnion' ou
[GOAL]
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
a : α
⊢ (∀ (i : Set α), i ∈ b ∧ a ∈ i → Set.Nonempty (i ∩ s)) ↔ ∀ (o : Set α), o ∈ b → a ∈ o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
simp only [and_imp]
[GOAL]
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ Dense s ↔ ∀ (o : Set α), o ∈ b → Set.Nonempty o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
simp only [Dense, hb.mem_closure_iff]
[GOAL]
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
⊢ (∀ (x : α) (o : Set α), o ∈ b → x ∈ o → Set.Nonempty (o ∩ s)) ↔
    ∀ (o : Set α), o ∈ b → Set.Nonempty o → Set.Nonempty (o ∩ s)
[PROOFSTEP]
exact ⟨fun h o hb ⟨a, ha⟩ => h a o hb ha, fun h a o hb ha => h o hb ⟨a, ha⟩⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
⊢ IsOpenMap f ↔ ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
[PROOFSTEP]
refine' ⟨fun H o ho => H _ (hB.isOpen ho), fun hf o ho => _⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (f '' o)
[PROOFSTEP]
rw [hB.open_eq_sUnion' ho, sUnion_eq_iUnion, image_iUnion]
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set α), s ∈ B → IsOpen (f '' s)
o : Set α
ho : IsOpen o
⊢ IsOpen (⋃ (i : ↑{s | s ∈ B ∧ s ⊆ o}), f '' ↑i)
[PROOFSTEP]
exact isOpen_iUnion fun s => hf s s.2.1
[GOAL]
α : Type u
t : TopologicalSpace α
⊢ ∀ (u : Set α), u ∈ {U | IsOpen U} → IsOpen u
[PROOFSTEP]
tauto
[GOAL]
α : Type u
t : TopologicalSpace α
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ {U | IsOpen U} ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
tauto
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ IsTopologicalBasis (image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂)
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds _ _
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (u : Set (α × β)), u ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ → IsOpen u
[PROOFSTEP]
rintro _ ⟨u₁, u₂, hu₁, hu₂, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
u₁ : Set α
u₂ : Set β
hu₁ : u₁ ∈ B₁
hu₂ : u₂ ∈ B₂
⊢ IsOpen ((fun x x_1 => x ×ˢ x_1) u₁ u₂)
[PROOFSTEP]
exact (h₁.isOpen hu₁).prod (h₂.isOpen hu₂)
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
⊢ ∀ (a : α × β) (u : Set (α × β)), a ∈ u → IsOpen u → ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rintro ⟨a, b⟩ u hu uo
[GOAL]
case refine'_2.mk
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu : (a, b) ∈ u
uo : IsOpen u
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
[PROOFSTEP]
rcases(h₁.nhds_hasBasis.prod_nhds h₂.nhds_hasBasis).mem_iff.1 (IsOpen.mem_nhds uo hu) with
  ⟨⟨s, t⟩, ⟨⟨hs, ha⟩, ht, hb⟩, hu⟩
[GOAL]
case refine'_2.mk.intro.mk.intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
a : α
b : β
u : Set (α × β)
hu✝ : (a, b) ∈ u
uo : IsOpen u
s : Set α
t : Set β
hu : (s, t).fst ×ˢ (s, t).snd ⊆ u
hs : (s, t).fst ∈ B₁
ha : a ∈ (s, t).fst
ht : (s, t).snd ∈ B₂
hb : b ∈ (s, t).snd
⊢ ∃ v, v ∈ image2 (fun x x_1 => x ×ˢ x_1) B₁ B₂ ∧ (a, b) ∈ v ∧ v ⊆ u
[PROOFSTEP]
exact ⟨s ×ˢ t, mem_image2_of_mem hs ht, ⟨ha, hb⟩, hu⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ IsTopologicalBasis (preimage f '' T)
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds _ _
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (u : Set α), u ∈ preimage f '' T → IsOpen u
[PROOFSTEP]
rintro _ ⟨V, hV, rfl⟩
[GOAL]
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ IsOpen (f ⁻¹' V)
[PROOFSTEP]
rw [hf.isOpen_iff]
[GOAL]
case refine'_1.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
V : Set β
hV : V ∈ T
⊢ ∃ t, IsOpen t ∧ f ⁻¹' t = f ⁻¹' V
[PROOFSTEP]
refine' ⟨V, h.isOpen hV, rfl⟩
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro a U ha hU
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
rw [hf.isOpen_iff] at hU
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
U : Set α
ha : a ∈ U
hU : ∃ t, IsOpen t ∧ f ⁻¹' t = U
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨V, hV, rfl⟩ := hU
[GOAL]
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
V : Set β
hV : IsOpen V
ha : a ∈ f ⁻¹' V
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' V
[PROOFSTEP]
obtain ⟨S, hS, rfl⟩ := h.open_eq_sUnion hV
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
ha : a ∈ f ⁻¹' ⋃₀ S
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
[PROOFSTEP]
obtain ⟨W, hW, ha⟩ := ha
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
f : α → β
T : Set (Set β)
hf : Inducing f
h : IsTopologicalBasis T
a : α
S : Set (Set β)
hS : S ⊆ T
hV : IsOpen (⋃₀ S)
W : Set β
hW : W ∈ S
ha : f a ∈ W
⊢ ∃ v, v ∈ preimage f '' T ∧ a ∈ v ∧ v ⊆ f ⁻¹' ⋃₀ S
[PROOFSTEP]
refine' ⟨f ⁻¹' W, ⟨_, hS hW, rfl⟩, ha, Set.preimage_mono <| Set.subset_sUnion_of_mem hW⟩
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Sort u_1
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 Subtype.val '' b i)
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds (fun u hu => _) _
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : u ∈ ⋃ (i : ι), image Subtype.val '' b i
⊢ IsOpen u
[PROOFSTEP]
simp only [mem_iUnion, mem_image] at hu
[GOAL]
case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ i x, x ∈ b i ∧ Subtype.val '' x = u
⊢ IsOpen u
[PROOFSTEP]
rcases hu with ⟨i, s, sb, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen (Subtype.val '' s)
[PROOFSTEP]
exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ ⋃ (i : ι), image Subtype.val '' b i ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro a u ha uo
[GOAL]
case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
⊢ ∃ v, v ∈ ⋃ (i : ι), image Subtype.val '' b i ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
[GOAL]
case refine'_2.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
i : ι
hi : a ∈ U i
⊢ ∃ v, v ∈ ⋃ (i : ι), image Subtype.val '' b i ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
lift a to ↥(U i) using hi
[GOAL]
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
⊢ ∃ v, v ∈ ⋃ (i : ι), image Subtype.val '' b i ∧ ↑a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rcases(hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with ⟨v, hvb, hav, hvu⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : ⋃ (i : ι), U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
v : Set ↑(U i)
hvb : v ∈ b i
hav : a ∈ v
hvu : v ⊆ Subtype.val ⁻¹' u
⊢ ∃ v, v ∈ ⋃ (i : ι), image Subtype.val '' b i ∧ ↑a ∈ v ∧ v ⊆ u
[PROOFSTEP]
exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav, image_subset_iff.2 hvu⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)
⊢ Continuous f
[PROOFSTEP]
rw [hB.eq_generateFrom]
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)
⊢ Continuous f
[PROOFSTEP]
exact continuous_generateFrom hf
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
⊢ ∃ u, DenseRange u
[PROOFSTEP]
obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
⊢ ∃ u, DenseRange u
[PROOFSTEP]
cases' Set.countable_iff_exists_subset_range.mp hs with u hu
[GOAL]
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : Nonempty α
s : Set α
hs : Set.Countable s
s_dense : Dense s
u : ℕ → α
hu : s ⊆ range u
⊢ ∃ u, DenseRange u
[PROOFSTEP]
exact ⟨u, s_dense.mono hu⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type ?u.24188
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
⊢ SeparableSpace (α × β)
[PROOFSTEP]
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type ?u.24188
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : Set.Countable s
hsd : Dense s
⊢ SeparableSpace (α × β)
[PROOFSTEP]
rcases exists_countable_dense β with ⟨t, htc, htd⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type ?u.24188
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : Set.Countable s
hsd : Dense s
t : Set β
htc : Set.Countable t
htd : Dense t
⊢ SeparableSpace (α × β)
[PROOFSTEP]
exact ⟨⟨s ×ˢ t, hsc.prod htc, hsd.prod htd⟩⟩
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
choose t htc htd using (exists_countable_dense <| X ·)
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
haveI := fun i ↦ (htc i).to_subtype
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
nontriviality ∀ i, X i
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
inhabit ∀ i, X i
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
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 _⟩
simp only [dif_pos hi]
exact hyu _
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
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
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
⊢ SeparableSpace ((i : ι) → X i)
[PROOFSTEP]
refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
⊢ Set.Nonempty (U ∩ range f)
[PROOFSTEP]
rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
[GOAL]
case intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
⊢ Set.Nonempty (U ∩ range f)
[PROOFSTEP]
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⟩
[GOAL]
case intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this✝ : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
this : ∀ (i : { x // x ∈ I }), ∃ y, y ∈ t ↑i ∧ y ∈ u ↑i
⊢ Set.Nonempty (U ∩ range f)
[PROOFSTEP]
choose y hyt hyu using this
[GOAL]
case intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
y : (i : { x // x ∈ I }) → X ↑i
hyt : ∀ (i : { x // x ∈ I }), y i ∈ t ↑i
hyu : ∀ (i : { x // x ∈ I }), y i ∈ u ↑i
⊢ Set.Nonempty (U ∩ range f)
[PROOFSTEP]
lift y to ∀ i : I, t i using hyt
[GOAL]
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
y : (i : { x // x ∈ I }) → ↑(t ↑i)
hyu : ∀ (i : { x // x ∈ I }), (fun i => ↑(y i)) i ∈ u ↑i
⊢ Set.Nonempty (U ∩ range f)
[PROOFSTEP]
refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
y : (i : { x // x ∈ I }) → ↑(t ↑i)
hyu : ∀ (i : { x // x ∈ I }), (fun i => ↑(y i)) i ∈ u ↑i
i : ι
hi : i ∈ I
⊢ f { fst := I, snd := y } i ∈ u i
[PROOFSTEP]
simp only [dif_pos hi]
[GOAL]
case intro.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), Set.Countable (t x)
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | { fst := I, snd := g } => if hi : i ∈ I then ↑(g { val := i, property := hi }) else default i
U : Set ((i : ι) → X i)
hU : IsOpen U
x✝ : Set.Nonempty U
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ (a : ι), a ∈ I → IsOpen (u a) ∧ g a ∈ u a
huU : Set.pi (↑I) u ⊆ U
y : (i : { x // x ∈ I }) → ↑(t ↑i)
hyu : ∀ (i : { x // x ∈ I }), (fun i => ↑(y i)) i ∈ u ↑i
i : ι
hi : i ∈ I
⊢ ↑(y { val := i, property := (_ : i ∈ I) }) ∈ u i
[PROOFSTEP]
exact hyu _
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ SeparableSpace α ↔ Countable α
[PROOFSTEP]
simp [SeparableSpace_iff, countable_univ_iff]
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
⊢ Set.Countable a
[PROOFSTEP]
rcases exists_countable_dense α with ⟨u, ⟨u_encodable⟩, u_dense⟩
[GOAL]
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
⊢ Set.Countable a
[PROOFSTEP]
have : ∀ i : a, ∃ y, y ∈ s i ∩ u := fun i => dense_iff_inter_open.1 u_dense (s i) (ha i i.2) (h'a i i.2)
[GOAL]
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
this : ∀ (i : ↑a), ∃ y, y ∈ s ↑i ∩ u
⊢ Set.Countable a
[PROOFSTEP]
choose f hfs hfu using this
[GOAL]
case intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
f : ↑a → α
hfs : ∀ (i : ↑a), f i ∈ s ↑i
hfu : ∀ (i : ↑a), f i ∈ u
⊢ Set.Countable a
[PROOFSTEP]
lift f to a → u using hfu
[GOAL]
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
f : ↑a → ↑u
hfs : ∀ (i : ↑a), (fun i => ↑(f i)) i ∈ s ↑i
⊢ Set.Countable a
[PROOFSTEP]
have f_inj : Injective f :=
  by
  refine' injective_iff_pairwise_ne.mpr ((h.subtype _ _).mono fun i j hij hfij => hij.le_bot ⟨hfs i, _⟩)
  simp only [congr_arg Subtype.val hfij, hfs j]
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
f : ↑a → ↑u
hfs : ∀ (i : ↑a), (fun i => ↑(f i)) i ∈ s ↑i
⊢ Injective f
[PROOFSTEP]
refine' injective_iff_pairwise_ne.mpr ((h.subtype _ _).mono fun i j hij hfij => hij.le_bot ⟨hfs i, _⟩)
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
f : ↑a → ↑u
hfs : ∀ (i : ↑a), (fun i => ↑(f i)) i ∈ s ↑i
i j : ↑a
hij : (Disjoint on s) ↑i ↑j
hfij : f i = f j
⊢ (fun i => ↑(f i)) i ∈ s ↑j
[PROOFSTEP]
simp only [congr_arg Subtype.val hfij, hfs j]
[GOAL]
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_1
s : ι → Set α
a : Set ι
h : PairwiseDisjoint a s
ha : ∀ (i : ι), i ∈ a → IsOpen (s i)
h'a : ∀ (i : ι), i ∈ a → Set.Nonempty (s i)
u : Set α
u_dense : Dense u
u_encodable : Encodable ↑u
f : ↑a → ↑u
hfs : ∀ (i : ↑a), (fun i => ↑(f i)) i ∈ s ↑i
f_inj : Injective f
⊢ Set.Countable a
[PROOFSTEP]
exact ⟨@Encodable.ofInj _ _ u_encodable f f_inj⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u
[PROOFSTEP]
rcases hs with ⟨c, c_count, hs⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : Set.Countable c
hs : s ⊆ closure c
⊢ IsSeparable u
[PROOFSTEP]
exact ⟨c, c_count, hu.trans hs⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : IsSeparable u
⊢ IsSeparable (s ∪ u)
[PROOFSTEP]
rcases hs with ⟨cs, cs_count, hcs⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
s u : Set α
hu : IsSeparable u
cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
⊢ IsSeparable (s ∪ u)
[PROOFSTEP]
rcases hu with ⟨cu, cu_count, hcu⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ IsSeparable (s ∪ u)
[PROOFSTEP]
refine' ⟨cs ∪ cu, cs_count.union cu_count, _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s u cs : Set α
cs_count : Set.Countable cs
hcs : s ⊆ closure cs
cu : Set α
cu_count : Set.Countable cu
hcu : u ⊆ closure cu
⊢ s ∪ u ⊆ closure (cs ∪ cu)
[PROOFSTEP]
exact
  union_subset (hcs.trans (closure_mono (subset_union_left _ _))) (hcu.trans (closure_mono (subset_union_right _ _)))
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
hs : IsSeparable s
⊢ IsSeparable (_root_.closure s)
[PROOFSTEP]
rcases hs with ⟨c, c_count, hs⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
s c : Set α
c_count : Set.Countable c
hs : s ⊆ _root_.closure c
⊢ IsSeparable (_root_.closure s)
[PROOFSTEP]
exact ⟨c, c_count, by simpa using closure_mono hs⟩
[GOAL]
α : Type u
t : TopologicalSpace α
s c : Set α
c_count : Set.Countable c
hs : s ⊆ _root_.closure c
⊢ _root_.closure s ⊆ _root_.closure c
[PROOFSTEP]
simpa using closure_mono hs
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (⋃ (i : ι), s i)
[PROOFSTEP]
choose c hc h'c using hs
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (⋃ (i : ι), s i)
[PROOFSTEP]
refine' ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => _⟩
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
inst✝ : Countable ι
s c : ι → Set α
hc : ∀ (i : ι), Set.Countable (c i)
h'c : ∀ (i : ι), s i ⊆ closure (c i)
i : ι
⊢ s i ⊆ closure (⋃ (i : ι), c i)
[PROOFSTEP]
exact (h'c i).trans (closure_mono (subset_iUnion _ i))
[GOAL]
α : Type u
t : TopologicalSpace α
⊢ IsSeparable univ ↔ SeparableSpace α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
t : TopologicalSpace α
⊢ IsSeparable univ → SeparableSpace α
[PROOFSTEP]
rintro ⟨c, c_count, hc⟩
[GOAL]
case mp.intro.intro
α : Type u
t : TopologicalSpace α
c : Set α
c_count : Set.Countable c
hc : univ ⊆ closure c
⊢ SeparableSpace α
[PROOFSTEP]
refine' ⟨⟨c, c_count, by rwa [dense_iff_closure_eq, ← univ_subset_iff]⟩⟩
[GOAL]
α : Type u
t : TopologicalSpace α
c : Set α
c_count : Set.Countable c
hc : univ ⊆ closure c
⊢ Dense c
[PROOFSTEP]
rwa [dense_iff_closure_eq, ← univ_subset_iff]
[GOAL]
case mpr
α : Type u
t : TopologicalSpace α
⊢ SeparableSpace α → IsSeparable univ
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
⊢ IsSeparable univ
[PROOFSTEP]
rcases exists_countable_dense α with ⟨c, c_count, hc⟩
[GOAL]
case mpr.intro.intro
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
c : Set α
c_count : Set.Countable c
hc : Dense c
⊢ IsSeparable univ
[PROOFSTEP]
exact ⟨c, c_count, by rwa [univ_subset_iff, ← dense_iff_closure_eq]⟩
[GOAL]
α : Type u
t : TopologicalSpace α
h : SeparableSpace α
c : Set α
c_count : Set.Countable c
hc : Dense c
⊢ univ ⊆ closure c
[PROOFSTEP]
rwa [univ_subset_iff, ← dense_iff_closure_eq]
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous f
⊢ IsSeparable (f '' s)
[PROOFSTEP]
rcases hs with ⟨c, c_count, hc⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ IsSeparable (f '' s)
[PROOFSTEP]
refine' ⟨f '' c, c_count.image _, _⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ f '' s ⊆ _root_.closure (f '' c)
[PROOFSTEP]
rw [image_subset_iff]
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set α
f : α → β
hf : Continuous f
c : Set α
c_count : Set.Countable c
hc : s ⊆ _root_.closure c
⊢ s ⊆ f ⁻¹' _root_.closure (f '' c)
[PROOFSTEP]
exact hc.trans (closure_subset_preimage_closure_image hf)
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
⊢ IsSeparable s
[PROOFSTEP]
have : IsSeparable (((↑) : s → α) '' (univ : Set s)) := (isSeparable_of_separableSpace _).image continuous_subtype_val
[GOAL]
α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
this : IsSeparable (Subtype.val '' univ)
⊢ IsSeparable s
[PROOFSTEP]
simpa only [image_univ, Subtype.range_val_subtype] using this
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
[PROOFSTEP]
refine' isTopologicalBasis_of_open_of_nhds _ _
[GOAL]
case refine'_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (u : Set ((i : ι) → X i)), u ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} → IsOpen u
[PROOFSTEP]
rintro _ ⟨U, F, h1, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ IsOpen (Set.pi (↑F) U)
[PROOFSTEP]
apply isOpen_set_pi F.finite_toSet
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ∀ (a : ι), a ∈ ↑F → IsOpen (U a)
[PROOFSTEP]
intro i hi
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
i : ι
hi : i ∈ ↑F
⊢ IsOpen (U i)
[PROOFSTEP]
exact (cond i).isOpen (h1 i hi)
[GOAL]
case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (a : (i : ι) → X i) (u : Set ((i : ι) → X i)),
    a ∈ u → IsOpen u → ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro a U ha hU
[GOAL]
case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨I, t, hta, htU⟩ : ∃ (I : Finset ι) (t : ∀ i : ι, Set (X i)), (∀ i, t i ∈ 𝓝 (a i)) ∧ Set.pi (↑I) t ⊆ U :=
  by
  rw [← Filter.mem_pi', ← nhds_pi]
  exact hU.mem_nhds ha
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (a i)) ∧ Set.pi (↑I) t ⊆ U
[PROOFSTEP]
rw [← Filter.mem_pi', ← nhds_pi]
[GOAL]
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ U ∈ 𝓝 fun i => a i
[PROOFSTEP]
exact hU.mem_nhds ha
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
have : ∀ i, ∃ V ∈ T i, a i ∈ V ∧ V ⊆ t i := fun i => (cond i).mem_nhds_iff.1 (hta i)
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
this : ∀ (i : ι), ∃ V, V ∈ T i ∧ a i ∈ V ∧ V ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
choose V hVT haV hVt using this
[GOAL]
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
V : (i : ι) → Set (X i)
hVT : ∀ (i : ι), V i ∈ T i
haV : ∀ (i : ι), a i ∈ V i
hVt : ∀ (i : ι), V i ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
[PROOFSTEP]
exact ⟨_, ⟨V, I, fun i _ => hVT i, rfl⟩, fun i _ => haV i, (pi_mono fun i _ => hVt i).trans htU⟩
[GOAL]
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
[PROOFSTEP]
letI := ⨅ i, induced (f i) (t i)
[GOAL]
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
[PROOFSTEP]
convert (isTopologicalBasis_pi cond).inducing (inducing_iInf_to_pi f)
[GOAL]
case h.e'_3
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
⊢ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} =
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
[PROOFSTEP]
ext V
[GOAL]
case h.e'_3.h
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} ↔
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
[PROOFSTEP]
constructor
[GOAL]
case h.e'_3.h.mp
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i} →
    V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
[PROOFSTEP]
rintro ⟨U, F, h1, rfl⟩
[GOAL]
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i ∈
    (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
[PROOFSTEP]
refine' ⟨(F : Set ι).pi U, ⟨U, F, h1, rfl⟩, _⟩
[GOAL]
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
[PROOFSTEP]
simp_rw [pi_def, Set.preimage_iInter]
[GOAL]
case h.e'_3.h.mp.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.h.mpr
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
V : Set β
⊢ V ∈ (preimage fun x i => f i x) '' {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} →
    V ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
[PROOFSTEP]
rintro ⟨U, ⟨U, F, h1, rfl⟩, rfl⟩
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U ∈
    {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}
[PROOFSTEP]
refine' ⟨U, F, h1, _⟩
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ (fun x i => f i x) ⁻¹' Set.pi (↑F) U = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
[PROOFSTEP]
simp_rw [pi_def, Set.preimage_iInter]
[GOAL]
case h.e'_3.h.mpr.intro.intro.intro.intro.intro
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
this : TopologicalSpace β := ⨅ (i : ι), induced (f i) (t i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ⋂ (i : ι) (_ : i ∈ ↑F), (fun x i => f i x) ⁻¹' (eval i ⁻¹' U i) = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
[PROOFSTEP]
rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
[PROOFSTEP]
refine' ⟨(t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s, _, _, _, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s ⊆ s
case intro.intro.intro.refine'_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Set.Countable ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)
case intro.intro.intro.refine'_3
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ Dense ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)
case intro.intro.intro.refine'_4
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
case intro.intro.intro.refine'_5
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : Set.Countable t
htd : Dense t
⊢ ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
[PROOFSTEP]
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⟩]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : SeparableSpace α
inst✝ : PartialOrder α
⊢ ∃ s, Set.Countable s ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
[PROOFSTEP]
simpa using dense_univ.exists_countable_dense_subset_bot_top
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type ?u.70125
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ IsCountablyGenerated (𝓝 (x, y))
[PROOFSTEP]
rw [nhds_prod_eq]
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type ?u.70125
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ IsCountablyGenerated (𝓝 x ×ˢ 𝓝 y)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
π : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), FirstCountableTopology (π i)
f : (i : ι) → π i
⊢ IsCountablyGenerated (𝓝 f)
[PROOFSTEP]
rw [nhds_pi]
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
π : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), FirstCountableTopology (π i)
f : (i : ι) → π i
⊢ IsCountablyGenerated (Filter.pi fun i => 𝓝 (f i))
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ IsTopologicalBasis b
[PROOFSTEP]
obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ IsTopologicalBasis b
[PROOFSTEP]
refine' ⟨_, _, not_mem_diff_of_mem _, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
[GOAL]
case intro.intro.refine'_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ Set.Countable ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ b} \ {∅})
case intro.intro.refine'_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}
[PROOFSTEP]
exacts [((countable_setOf_finite_subset hb₁).image _).mono (diff_subset _ _), rfl]
[GOAL]
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α
[PROOFSTEP]
rcases@SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
⊢ SecondCountableTopology α
[PROOFSTEP]
letI := t.induced f
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α
[PROOFSTEP]
refine' { is_open_generated_countable := ⟨preimage f '' b, hb.image _, _⟩ }
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)
[PROOFSTEP]
rw [eq, induced_generateFrom_eq]
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Sort u_1
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α
[PROOFSTEP]
rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]
[GOAL]
α : Type u
t✝ : TopologicalSpace α
ι : Sort u_1
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α
[PROOFSTEP]
exact
  SecondCountableTopology.mk' <|
    countable_iUnion fun i =>
      @countable_countableBasis _ (t i)
        (ht i)
          -- TODO: more fine grained instances for first_countable_topology, separable_space, t2_space, ...
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ SeparableSpace α
[PROOFSTEP]
choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
p : ↑(countableBasis α) → α
hp : ∀ (s : ↑(countableBasis α)), p s ∈ ↑s
⊢ SeparableSpace α
[PROOFSTEP]
exact
  ⟨⟨range p, countable_range _,
      (isBasis_countableBasis α).dense_iff.2 fun o ho _ => ⟨p ⟨o, ho⟩, hp _, mem_range_self _⟩⟩⟩
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
⊢ ∃ T, Set.Countable T ∧ ⋃ (i : ι) (_ : i ∈ T), s i = ⋃ (i : ι), s i
[PROOFSTEP]
let B := {b ∈ countableBasis α | ∃ i, b ⊆ s i}
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
⊢ ∃ T, Set.Countable T ∧ ⋃ (i : ι) (_ : i ∈ T), s i = ⋃ (i : ι), s i
[PROOFSTEP]
choose f hf using fun b : B => b.2.2
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
⊢ ∃ T, Set.Countable T ∧ ⋃ (i : ι) (_ : i ∈ T), s i = ⋃ (i : ι), s i
[PROOFSTEP]
haveI : Encodable B := ((countable_countableBasis α).mono (sep_subset _ _)).toEncodable
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Encodable ↑B
⊢ ∃ T, Set.Countable T ∧ ⋃ (i : ι) (_ : i ∈ T), s i = ⋃ (i : ι), s i
[PROOFSTEP]
refine' ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset _)⟩
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Encodable ↑B
⊢ ∀ (t' : Set α), (t' ∈ range fun i => s i) → t' ⊆ ⋃ (i : ι) (_ : i ∈ range f), s i
[PROOFSTEP]
rintro _ ⟨i, rfl⟩ x xs
[GOAL]
case intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Encodable ↑B
i : ι
x : α
xs : x ∈ (fun i => s i) i
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ range f), s i
[PROOFSTEP]
rcases(isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
[GOAL]
case intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen (s i)
B : Set (Set α) := {b | b ∈ countableBasis α ∧ ∃ i, b ⊆ s i}
f : ↑B → ι
hf : ∀ (b : ↑B), ↑b ⊆ s (f b)
this : Encodable ↑B
i : ι
x : α
xs : x ∈ (fun i => s i) i
b : Set α
hb : b ∈ countableBasis α
xb : x ∈ b
bs : b ⊆ (fun i => s i) i
⊢ x ∈ ⋃ (i : ι) (_ : i ∈ range f), s i
[PROOFSTEP]
exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ (s : Set α), s ∈ S → IsOpen s
T : Set ↑S
cT : Set.Countable T
hT : ⋃ (i : ↑S) (_ : i ∈ T), ↑i = ⋃ (i : ↑S), ↑i
⊢ ⋃₀ (Subtype.val '' T) = ⋃₀ S
[PROOFSTEP]
rwa [sUnion_image, sUnion_eq_iUnion]
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ s, Set.Countable s ∧ ⋃ (x : α) (_ : x ∈ s), f x = univ
[PROOFSTEP]
rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with ⟨s, hsc, hsU⟩
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : ⋃ (i : α) (_ : i ∈ s), interior (f i) = ⋃ (i : α), interior (f i)
⊢ ∃ s, Set.Countable s ∧ ⋃ (x : α) (_ : x ∈ s), f x = univ
[PROOFSTEP]
suffices : ⋃ x ∈ s, interior (f x) = univ
[GOAL]
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : ⋃ (i : α) (_ : i ∈ s), interior (f i) = ⋃ (i : α), interior (f i)
this : ⋃ (x : α) (_ : x ∈ s), interior (f x) = univ
⊢ ∃ s, Set.Countable s ∧ ⋃ (x : α) (_ : x ∈ s), f x = univ
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : ⋃ (i : α) (_ : i ∈ s), interior (f i) = ⋃ (i : α), interior (f i)
⊢ ⋃ (x : α) (_ : x ∈ s), interior (f x) = univ
[PROOFSTEP]
exact ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
[GOAL]
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : ⋃ (i : α) (_ : i ∈ s), interior (f i) = ⋃ (i : α), interior (f i)
⊢ ⋃ (x : α) (_ : x ∈ s), interior (f x) = univ
[PROOFSTEP]
simp only [hsU, eq_univ_iff_forall, mem_iUnion]
[GOAL]
case this
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : Set.Countable s
hsU : ⋃ (i : α) (_ : i ∈ s), interior (f i) = ⋃ (i : α), interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)
[PROOFSTEP]
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
[PROOFSTEP]
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)
[GOAL]
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
[PROOFSTEP]
rcases countable_cover_nhds this with ⟨t, htc, htU⟩
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : ⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x = univ
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
[PROOFSTEP]
refine' ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => _⟩
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : ⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (x : α) (_ : x ∈ Subtype.val '' t), f x
[PROOFSTEP]
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢
[GOAL]
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ (i : ↑s) (_ : i ∈ t), f ↑i
⊢ x ∈ ⋃ (y : ↑s) (_ : y ∈ t), f ↑y
[PROOFSTEP]
exact htU ⟨x, hx⟩
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i)
[PROOFSTEP]
apply isTopologicalBasis_of_open_of_nhds
[GOAL]
case h_open
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ ∀ (u : Set ((i : ι) × E i)), u ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i → IsOpen u
[PROOFSTEP]
intro u hu
[GOAL]
case h_open
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
u : Set ((i : ι) × E i)
hu : u ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i
⊢ IsOpen u
[PROOFSTEP]
obtain ⟨i, t, ts, rfl⟩ : ∃ (i : ι) (t : Set (E i)), t ∈ s i ∧ Sigma.mk i '' t = u := by
  simpa only [mem_iUnion, mem_image] using hu
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
u : Set ((i : ι) × E i)
hu : u ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i
⊢ ∃ i t, t ∈ s i ∧ Sigma.mk i '' t = u
[PROOFSTEP]
simpa only [mem_iUnion, mem_image] using hu
[GOAL]
case h_open.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
i : ι
t : Set (E i)
ts : t ∈ s i
hu : Sigma.mk i '' t ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i
⊢ IsOpen (Sigma.mk i '' t)
[PROOFSTEP]
exact isOpenMap_sigmaMk _ ((hs i).isOpen ts)
[GOAL]
case h_nhds
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ ∀ (a : (i : ι) × E i) (u : Set ((i : ι) × E i)),
    a ∈ u → IsOpen u → ∃ v, v ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rintro ⟨i, x⟩ u hxu u_open
[GOAL]
case h_nhds.mk
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
i : ι
x : E i
u : Set ((i : ι) × E i)
hxu : { fst := i, snd := x } ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i ∧ { fst := i, snd := x } ∈ v ∧ v ⊆ u
[PROOFSTEP]
have hx : x ∈ Sigma.mk i ⁻¹' u := hxu
[GOAL]
case h_nhds.mk
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
i : ι
x : E i
u : Set ((i : ι) × E i)
hxu : { fst := i, snd := x } ∈ u
u_open : IsOpen u
hx : x ∈ Sigma.mk i ⁻¹' u
⊢ ∃ v, v ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i ∧ { fst := i, snd := x } ∈ v ∧ v ⊆ u
[PROOFSTEP]
obtain ⟨v, vs, xv, hv⟩ : ∃ (v : Set (E i)), v ∈ s i ∧ x ∈ v ∧ v ⊆ Sigma.mk i ⁻¹' u :=
  (hs i).exists_subset_of_mem_open hx (isOpen_sigma_iff.1 u_open i)
[GOAL]
case h_nhds.mk.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
i : ι
x : E i
u : Set ((i : ι) × E i)
hxu : { fst := i, snd := x } ∈ u
u_open : IsOpen u
hx : x ∈ Sigma.mk i ⁻¹' u
v : Set (E i)
vs : v ∈ s i
xv : x ∈ v
hv : v ⊆ Sigma.mk i ⁻¹' u
⊢ ∃ v, v ∈ ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' s i ∧ { fst := i, snd := x } ∈ v ∧ v ⊆ u
[PROOFSTEP]
exact ⟨Sigma.mk i '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ vs⟩, mem_image_of_mem _ xv, image_subset_iff.2 hv⟩
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
⊢ SecondCountableTopology ((i : ι) × E i)
[PROOFSTEP]
let b := ⋃ i : ι, (fun u => (Sigma.mk i '' u : Set (Σ i, E i))) '' countableBasis (E i)
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
b : Set (Set ((i : ι) × E i)) := ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' countableBasis (E i)
⊢ SecondCountableTopology ((i : ι) × E i)
[PROOFSTEP]
have A : IsTopologicalBasis b := IsTopologicalBasis.sigma fun i => isBasis_countableBasis _
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
b : Set (Set ((i : ι) × E i)) := ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
⊢ SecondCountableTopology ((i : ι) × E i)
[PROOFSTEP]
have B : b.Countable := countable_iUnion fun i => (countable_countableBasis _).image _
[GOAL]
α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
b : Set (Set ((i : ι) × E i)) := ⋃ (i : ι), (fun u => Sigma.mk i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
B : Set.Countable b
⊢ SecondCountableTopology ((i : ι) × E i)
[PROOFSTEP]
exact A.secondCountableTopology B
[GOAL]
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
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)
[PROOFSTEP]
apply isTopologicalBasis_of_open_of_nhds
[GOAL]
case h_open
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (u : Set (α ⊕ β)), u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t → IsOpen u
[PROOFSTEP]
rintro u (⟨w, hw, rfl⟩ | ⟨w, hw, rfl⟩)
[GOAL]
case h_open.inl.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen ((fun u => Sum.inl '' u) w)
[PROOFSTEP]
exact openEmbedding_inl.isOpenMap w (hs.isOpen hw)
[GOAL]
case h_open.inr.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen ((fun u => Sum.inr '' u) w)
[PROOFSTEP]
exact openEmbedding_inr.isOpenMap w (ht.isOpen hw)
[GOAL]
case h_nhds
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u → IsOpen u → ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rintro (x | x) u hxu u_open
[GOAL]
case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u
[PROOFSTEP]
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
[GOAL]
case h_nhds.inl.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inl x ∈ v ∧ v ⊆ u
[PROOFSTEP]
exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv, image_subset_iff.2 vu⟩
[GOAL]
case h_nhds.inr
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
[PROOFSTEP]
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
[GOAL]
case h_nhds.inr.intro.intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ v, v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t ∧ Sum.inr x ∈ v ∧ v ⊆ u
[PROOFSTEP]
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv, image_subset_iff.2 vu⟩
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
⊢ SecondCountableTopology (α ⊕ β)
[PROOFSTEP]
let b := (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
⊢ SecondCountableTopology (α ⊕ β)
[PROOFSTEP]
have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
⊢ SecondCountableTopology (α ⊕ β)
[PROOFSTEP]
have B : b.Countable :=
  (Countable.image (countable_countableBasis _) _).union (Countable.image (countable_countableBasis _) _)
[GOAL]
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u => Sum.inl '' u) '' countableBasis α ∪ (fun u => Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
B : Set.Countable b
⊢ SecondCountableTopology (α ⊕ β)
[PROOFSTEP]
exact A.secondCountableTopology B
[GOAL]
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)
[PROOFSTEP]
apply isTopologicalBasis_of_open_of_nhds
[GOAL]
case h_open
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (u : Set Y), u ∈ image π '' V → IsOpen u
[PROOFSTEP]
rintro - ⟨U, U_in_V, rfl⟩
[GOAL]
case h_open.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen (π '' U)
[PROOFSTEP]
apply h U (hV.isOpen U_in_V)
[GOAL]
case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
⊢ ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen u → ∃ v, v ∈ image π '' V ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
intro y U y_in_U U_open
[GOAL]
case h_nhds
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen U
⊢ ∃ v, v ∈ image π '' V ∧ y ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨x, rfl⟩ := h'.surjective y
[GOAL]
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
let W := π ⁻¹' U
[GOAL]
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
have x_in_W : x ∈ W := y_in_U
[GOAL]
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
have W_open : IsOpen W := U_open.preimage h'.continuous
[GOAL]
case h_nhds.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open
[GOAL]
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
have πZ_in_U : π '' Z ⊆ U := (Set.image_subset _ Z_in_W).trans (image_preimage_subset π U)
[GOAL]
case h_nhds.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : QuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
πZ_in_U : π '' Z ⊆ U
⊢ ∃ v, v ∈ image π '' V ∧ π x ∈ v ∧ v ⊆ U
[PROOFSTEP]
exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, πZ_in_U⟩
[GOAL]
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : QuotientMap π
h : IsOpenMap π
⊢ ∃ b, Set.Countable b ∧ inst✝¹ = generateFrom b
[PROOFSTEP]
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
[GOAL]
case intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : QuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : Set.Countable V
V_generates : IsTopologicalBasis V
⊢ ∃ b, Set.Countable b ∧ inst✝¹ = generateFrom b
[PROOFSTEP]
exact ⟨Set.image π '' V, V_countable.image (Set.image π), (V_generates.quotientMap h' h).eq_generateFrom⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : SecondCountableTopology β
hf : Inducing f
⊢ SecondCountableTopology α
[PROOFSTEP]
rw [hf.1]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
inst✝ : SecondCountableTopology β
hf : Inducing f
⊢ SecondCountableTopology α
[PROOFSTEP]
exact secondCountableTopology_induced α β f