α : Type u
β : Type v
ι : Type ?u.35600
π : ι → Type ?u.35605
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (⋃ (b : Bool), bif b then s else t)
α : Type u
β : Type v
ι : Type ?u.35600
π : ι → Type ?u.35605
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ∪ t)
rw [union_eq_iUnion]
no goals
α : Type u
β : Type v
ι : Type ?u.35600
π : ι → Type ?u.35605
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (⋃ (b : Bool), bif b then s else t)
exact isCompact_iUnion fun b => by cases b <;> assumption
no goals
α : Type u
β : Type v
ι : Type ?u.35600
π : ι → Type ?u.35605
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)
cases b <;> assumption