R₁ : Type ?u.2937
R₂ : Type ?u.2940
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_2
M₂ : Type u_1
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ (∃ V, V ∈ 𝓝 0 ∧ ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V, V ∈ 𝓝 0 ∧ IsCompact (closure (f '' V))
R₁ : Type ?u.2937
R₂ : Type ?u.2940
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_2
M₂ : Type u_1
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔ ∃ V, V ∈ 𝓝 0 ∧ IsCompact (closure (f '' V))
rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]
no goals
R₁ : Type ?u.2937
R₂ : Type ?u.2940
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_2
M₂ : Type u_1
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ (∃ V, V ∈ 𝓝 0 ∧ ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V, V ∈ 𝓝 0 ∧ IsCompact (closure (f '' V))
exact
  ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, isCompact_closure_of_subset_compact hK hKV⟩,
    fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩