case ht
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ∀ (a : α), a ∈ Set.ite t s s' ∩ frontier t → f a = f' a

case hf
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f (Set.ite t s s' ∩ closure t)

case hg
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f' (Set.ite t s s' ∩ closure (tᶜ))
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn (piecewise t f f') (Set.ite t s s')
apply ContinuousOn.piecewise
no goals
case ht
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ∀ (a : α), a ∈ Set.ite t s s' ∩ frontier t → f a = f' a
rwa [ite_inter_of_inter_eq _ H]
no goals
case hf
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f (Set.ite t s s' ∩ closure t)
rwa [ite_inter_closure_eq_of_inter_frontier_eq H]
no goals
case hg
α : Type u_1
β : Type u_2
γ : Type ?u.399126
δ : Type ?u.399129
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s s' t : Set α
f f' : α → β
inst✝ : (x : α) → Decidable (x ∈ t)
h : ContinuousOn f (s ∩ closure t)
h' : ContinuousOn f' (s' ∩ closure (tᶜ))
H : s ∩ frontier t = s' ∩ frontier t
Heq : EqOn f f' (s ∩ frontier t)
⊢ ContinuousOn f' (Set.ite t s s' ∩ closure (tᶜ))
rwa [ite_inter_closure_compl_eq_of_inter_frontier_eq H]