case mp
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ s ∈ residual α → ∃ t x, IsGδ t ∧ Dense t

case mpr
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ t x, IsGδ t ∧ Dense t) → s ∈ residual α
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ s ∈ residual α ↔ ∃ t x, IsGδ t ∧ Dense t
constructor
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual α
case mpr
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ t x, IsGδ t ∧ Dense t) → s ∈ residual α
rintro ⟨t, ts, ho, hd⟩
no goals
case mpr.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s t : Set α
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual α
exact mem_of_superset (residual_of_dense_Gδ ho hd) ts
case mp
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) →
    ∃ t x, IsGδ t ∧ Dense t
case mp
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ s ∈ residual α → ∃ t x, IsGδ t ∧ Dense t
rw [mem_residual_iff]
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ ∃ t x, IsGδ t ∧ Dense t
case mp
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
⊢ (∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) →
    ∃ t x, IsGδ t ∧ Dense t
rintro ⟨S, hSo, hSd, Sct, Ss⟩
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ ∃ t x, IsGδ t ∧ Dense t
refine' ⟨_, Ss, ⟨_, fun t ht => hSo _ ht, Sct, rfl⟩, _⟩
no goals
case mp.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14520
γ : Type ?u.14523
ι : Type ?u.14526
inst✝¹ : TopologicalSpace α
inst✝ : BaireSpace α
s : Set α
S : Set (Set α)
hSo : ∀ (t : Set α), t ∈ S → IsOpen t
hSd : ∀ (t : Set α), t ∈ S → Dense t
Sct : Set.Countable S
Ss : ⋂₀ S ⊆ s
⊢ Dense (⋂₀ S)
exact dense_sInter_of_open hSo Sct hSd