ι : Type u_1
ι' : Type u_3
α : Type ?u.1343
X : Type u_2
Y : Type ?u.1349
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
ι : Type u_1
ι' : Type u_3
α : Type ?u.1343
X : Type u_2
Y : Type ?u.1349
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
let ⟨t, htx, htf⟩ := hf x
ι : Type u_1
ι' : Type u_3
α : Type ?u.1343
X : Type u_2
Y : Type ?u.1349
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ InjOn (fun i => g i) ((fun i => g i) ⁻¹' {i | Set.Nonempty (f i ∩ t)})
ι : Type u_1
ι' : Type u_3
α : Type ?u.1343
X : Type u_2
Y : Type ?u.1349
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((f ∘ g) i ∩ t)}
refine ⟨t, htx, htf.preimage <| ?_⟩
no goals
ι : Type u_1
ι' : Type u_3
α : Type ?u.1343
X : Type u_2
Y : Type ?u.1349
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : ι' → ι
hf : LocallyFinite f
hg : InjOn g {i | Set.Nonempty (f (g i))}
x : X
t : Set X
htx : t ∈ 𝓝 x
htf : Set.Finite {i | Set.Nonempty (f i ∩ t)}
⊢ InjOn (fun i => g i) ((fun i => g i) ⁻¹' {i | Set.Nonempty (f i ∩ t)})
exact hg.mono fun i (hi : Set.Nonempty _) => hi.left