α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ N ∈ map f (cocompact α)
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
⊢ Tendsto f (cocompact α) (𝓝 1)
intro N hN
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ N ∈ map f (cocompact α)
rw [mem_map, mem_cocompact']
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ ∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
refine' ⟨mulTSupport f, h.isCompact, _⟩
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ mulTSupport fᶜ ⊆ f ⁻¹' N
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ (f ⁻¹' N)ᶜ ⊆ mulTSupport f
rw [compl_subset_comm]
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ mulTSupport fᶜ
⊢ v ∈ f ⁻¹' N
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
⊢ mulTSupport fᶜ ⊆ f ⁻¹' N
intro v hv
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ mulTSupport fᶜ
⊢ 1 ∈ N
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ mulTSupport fᶜ
⊢ v ∈ f ⁻¹' N
rw [mem_preimage, image_eq_one_of_nmem_mulTSupport hv]
no goals
α : Type u_2
β : Type ?u.45460
γ : Type u_1
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
f : α → γ
inst✝¹ : TopologicalSpace γ
inst✝ : One γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ mulTSupport fᶜ
⊢ 1 ∈ N
exact mem_of_mem_nhds hN