α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (⋃ (b : Bool), bif b then s₁ else s₂)
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (s₁ ∪ s₂)
rw [union_eq_iUnion]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (⋃ (b : Bool), bif b then s₁ else s₂)
exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)