α : 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
α : 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
let B := { b ∈ countableBasis α | ∃ i, b ⊆ s i }
α : 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
α : 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
choose f hf using fun b : B => b.2.2
α : 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
α : 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
haveI : Encodable B := ((countable_countableBasis α).mono (sep_subset _ _)).toEncodable
α : 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
α : 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
refine' ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset _)⟩
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
α : 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
rintro _ ⟨i, rfl⟩ x xs
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
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
rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
no goals
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
exact ⟨_, ⟨_, rfl⟩, _, ⟨⟨⟨_, hb, _, bs⟩, rfl⟩, rfl⟩, hf _ xb⟩