case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (g ∘ f)
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
hf : IsCompactOperator f
g : M₂ → M₃
hg : Continuous g
⊢ IsCompactOperator (g ∘ f)
rcases hf with ⟨K, hK, hKf⟩
case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)
case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ IsCompactOperator (g ∘ f)
refine' ⟨g '' K, hK.image hg, mem_of_superset hKf _⟩
case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))
case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ g ∘ f ⁻¹' (g '' K)
rw [preimage_comp]
no goals
case intro.intro
R₁ : Type ?u.179451
R₂ : Type ?u.179454
R₃ : Type ?u.179457
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
inst✝⁴ : TopologicalSpace M₁
inst✝³ : TopologicalSpace M₂
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
f : M₁ → M₂
g : M₂ → M₃
hg : Continuous g
K : Set M₂
hK : IsCompact K
hKf : f ⁻¹' K ∈ 𝓝 0
⊢ f ⁻¹' K ⊆ f ⁻¹' (g ⁻¹' (g '' K))
exact preimage_mono (subset_preimage_image _ _)