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
α : 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
rcases exists_countable_dense α with ⟨u, ⟨u_encodable⟩, u_dense⟩
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
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
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)
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
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
choose f hfs hfu using this
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
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
lift f to a → u using hfu
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
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
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]
no goals
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
exact ⟨@Encodable.ofInj _ _ u_encodable f f_inj⟩
α : 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
α : 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
refine' injective_iff_pairwise_ne.mpr
  ((h.subtype _ _).mono fun i j hij hfij => hij.le_bot ⟨hfs i, _⟩)
no goals
α : 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
simp only [congr_arg Subtype.val hfij, hfs j]