α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hf : Continuous f
⊢ ∀ (i' : Set α), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hf : Continuous f
⊢ comap f (cocompact β) ≤ cocompact α
rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : α → β
hf : Continuous f
t : Set α
ht : IsCompact t
⊢ ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hf : Continuous f
⊢ ∀ (i' : Set α), IsCompact i' → ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
intro t ht
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : α → β
hf : Continuous f
t : Set α
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : α → β
hf : Continuous f
t : Set α
ht : IsCompact t
⊢ ∃ i, IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ
refine' ⟨f '' t, ht.image hf, _⟩
no goals
α : Type u
β : Type v
ι : Type ?u.89720
π : ι → Type ?u.89725
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
f : α → β
hf : Continuous f
t : Set α
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
simpa using t.subset_preimage_image f