α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
⊢ ∀ (t : Set α), (t ⊆ ⋃ (i : ι), f i) → IsCompact t
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ (i : ι), f i)
simp_rw [noetherianSpace_set_iff] at hf ⊢
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact t
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
⊢ ∀ (t : Set α), (t ⊆ ⋃ (i : ι), f i) → IsCompact t
intro t ht
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact (⋃ (i : ι), t ∩ f i)
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact t
rw [← Set.inter_eq_left_iff_subset.mpr ht, Set.inter_iUnion]
no goals
α : Type u_2
β : Type ?u.6819
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_1
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact (⋃ (i : ι), t ∩ f i)
exact isCompact_iUnion fun i => hf i _ (Set.inter_subset_right _ _)