no goals
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
⊢ IsOpen (Set.ite t s s')
classical
  simp only [isOpen_iff_continuous_mem, Set.ite] at *
  convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn
  rename_i x
  by_cases hx : x ∈ t <;> simp [hx]
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
⊢ Continuous fun x => x ∈ s ∩ t ∪ s' \ t
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
⊢ IsOpen (Set.ite t s s')
simp only [isOpen_iff_continuous_mem, Set.ite] at *
case h.e'_5.h.a
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x✝
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
⊢ Continuous fun x => x ∈ s ∩ t ∪ s' \ t
convert continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn
case h.e'_5.h.a
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x
case h.e'_5.h.a
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x✝
rename_i x
no goals
case h.e'_5.h.a
α : Type u_1
β : Type ?u.385864
γ : Type ?u.385867
δ : Type ?u.385870
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s s' t : Set α
ht : ∀ (x : α), x ∈ frontier t → (x ∈ s ↔ x ∈ s')
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ piecewise t (fun x => x ∈ s) (fun x => x ∈ s') x
by_cases hx : x ∈ t <;> simp [hx]