α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
⊢ Dense (⋃ (i : ι), interior (f i))
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
⊢ Dense (⋃ (i : ι), interior (f i))
let g i := frontier (f i)ᶜ
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋃ (i : ι), interior (f i))
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
⊢ Dense (⋃ (i : ι), interior (f i))
have hgo : ∀ i, IsOpen (g i) := fun i => isClosed_frontier.isOpen_compl
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ Dense (⋃ (i : ι), interior (f i))
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋃ (i : ι), interior (f i))
have hgd : Dense (⋂ i, g i) := by
  refine' dense_iInter_of_open hgo fun i x => _
  rw [closure_compl, interior_frontier (hc _)]
  exact id
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ (s ∩ ⋂ (i : ι), g i) ⊆ ⋃ (i : ι), interior (f i)
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ Dense (⋃ (i : ι), interior (f i))
refine' (hd.inter_of_Gδ hs (isGδ_iInter_of_open fun i => (hgo i)) hgd).mono _
case intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : x ∈ ⋂ (i : ι), g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
⊢ (s ∩ ⋂ (i : ι), g i) ⊆ ⋃ (i : ι), interior (f i)
rintro x ⟨hxs, hxg⟩
case intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
case intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : x ∈ ⋂ (i : ι), g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
rw [mem_iInter] at hxg
case intro.intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ (i : ι), interior (f i)
case intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ (i : ι), interior (f i)
rcases mem_iUnion.1 (hU hxs) with ⟨i, hi⟩
no goals
case intro.intro
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
hgd : Dense (⋂ (i : ι), g i)
x : α
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
i : ι
hi : x ∈ f i
⊢ x ∈ ⋃ (i : ι), interior (f i)
exact mem_iUnion.2 ⟨i, self_diff_frontier (f i) ▸ ⟨hi, hxg _⟩⟩
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ closure (g i)
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
⊢ Dense (⋂ (i : ι), g i)
refine' dense_iInter_of_open hgo fun i x => _
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ ∅ᶜ
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ closure (g i)
rw [closure_compl, interior_frontier (hc _)]
no goals
α : Type u_2
β : Type ?u.24679
γ : Type ?u.24682
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : BaireSpace α
inst✝ : Encodable ι
s : Set α
hs : IsGδ s
hd : Dense s
f : ι → Set α
hc : ∀ (i : ι), IsClosed (f i)
hU : s ⊆ ⋃ (i : ι), f i
g : ι → Set α := fun i => frontier (f i)ᶜ
hgo : ∀ (i : ι), IsOpen (g i)
i : ι
x : α
⊢ x ∈ ∅ᶜ
exact id