X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))
refine' isCompact_of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure _
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
rw [hg.toEmbedding.closure_eq_preimage_closure_image]
no goals
X : Type ?u.15456
α : Type u_1
α' : Type u_3
β : Type u_2
γ : Type ?u.15468
δ : Type ?u.15471
M : Type ?u.15474
E : Type ?u.15477
R : Type ?u.15480
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f
exact preimage_mono (closure_mono <| image_preimage_subset _ _)