case inl
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : S = ∅
⊢ Dense (⋂₀ S)

case inr
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
⊢ Dense (⋂₀ S)
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
⊢ Dense (⋂₀ S)
cases' S.eq_empty_or_nonempty with h h
no goals
case inl
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : S = ∅
⊢ Dense (⋂₀ S)
simp [h]
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
⊢ Dense (⋂₀ S)
case inr
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
⊢ Dense (⋂₀ S)
rcases hS.exists_eq_range h with ⟨f, hf⟩
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂₀ S)
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
⊢ Dense (⋂₀ S)
have F : ∀ n, f n ∈ S := fun n => by rw [hf]; exact mem_range_self _
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂ (x : ℕ), f x)
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂₀ S)
rw [hf, sInter_range]
no goals
case inr.intro
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
F : ∀ (n : ℕ), f n ∈ S
⊢ Dense (⋂ (x : ℕ), f x)
exact dense_iInter_of_open_nat (fun n => ho _ (F n)) fun n => hd _ (F n)
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
n : ℕ
⊢ f n ∈ range f
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
n : ℕ
⊢ f n ∈ S
rw [hf]
no goals
α : Type u_1
β : Type ?u.12812
γ : Type ?u.12815
ι : Type ?u.12818
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
S : Set (Set α)
ho : ∀ (s : Set α), s ∈ S → IsOpen s
hS : Set.Countable S
hd : ∀ (s : Set α), s ∈ S → Dense s
h : Set.Nonempty S
f : ℕ → Set α
hf : S = range f
n : ℕ
⊢ f n ∈ range f
exact mem_range_self _