ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
⊢ ContinuousOn g (⋃ (i : ι), f i)
rintro x -
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ContinuousWithinAt g (⋃ (i : ι), f i) x
rw [ContinuousWithinAt, hf.nhdsWithin_iUnion, tendsto_iSup]
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
⊢ ∀ (i : ι), Tendsto g (𝓝[f i] x) (𝓝 (g x))
intro i
case pos
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
by_cases hx : x ∈ closure (f i)
no goals
case pos
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
exact hc i _ hx
case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : ¬x ∈ closure (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot] at hx
case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))
case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
rw [hx]
no goals
case neg
ι : Type u_1
ι' : Type ?u.4835
α : Type ?u.4838
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g✝ : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι) (x : X), x ∈ closure (f i) → ContinuousWithinAt g (f i) x
x : X
i : ι
hx : 𝓝[f i] x = ⊥
⊢ Tendsto g ⊥ (𝓝 (g x))
exact tendsto_bot