α : Type u
β : Type v
ι : Type ?u.32535
π : ι → Type ?u.32540
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (Set α)
hf : Set.Finite S
hc : ∀ (s : Set α), s ∈ S → IsCompact s
⊢ IsCompact (⋃ (i : Set α) (_ : i ∈ S), i)
α : Type u
β : Type v
ι : Type ?u.32535
π : ι → Type ?u.32540
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (Set α)
hf : Set.Finite S
hc : ∀ (s : Set α), s ∈ S → IsCompact s
⊢ IsCompact (⋃₀ S)
rw [sUnion_eq_biUnion]
no goals
α : Type u
β : Type v
ι : Type ?u.32535
π : ι → Type ?u.32540
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
S : Set (Set α)
hf : Set.Finite S
hc : ∀ (s : Set α), s ∈ S → IsCompact s
⊢ IsCompact (⋃ (i : Set α) (_ : i ∈ S), i)
exact hf.isCompact_biUnion hc