α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : (⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x) = univ
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
rcases countable_cover_nhds this with ⟨t, htc, htU⟩
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : (⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x) = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (x : α) (_ : x ∈ Subtype.val '' t), f x
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : (⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x) = univ
⊢ ∃ t, t ⊆ s ∧ Set.Countable t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), f x
refine' ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => _⟩
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ (i : ↑s) (_ : i ∈ t), f ↑i
⊢ x ∈ ⋃ (y : ↑s) (_ : y ∈ t), f ↑y
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
htU : (⋃ (x : ↑s) (_ : x ∈ t), Subtype.val ⁻¹' f ↑x) = univ
x : α
hx : x ∈ s
⊢ x ∈ ⋃ (x : α) (_ : x ∈ Subtype.val '' t), f x
simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU⊢
no goals
case intro.intro
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ (x : α), x ∈ s → f x ∈ 𝓝[s] x
this : ∀ (x : ↑s), Subtype.val ⁻¹' f ↑x ∈ 𝓝 x
t : Set ↑s
htc : Set.Countable t
x : α
hx : x ∈ s
htU : ∀ (x : ↑s), ↑x ∈ ⋃ (i : ↑s) (_ : i ∈ t), f ↑i
⊢ x ∈ ⋃ (y : ↑s) (_ : y ∈ t), f ↑y
exact htU ⟨x, hx⟩