α : Type u
β : Type v
ι : Type ?u.179439
π : ι → Type ?u.179444
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ Continuous (restrict s (boolIndicator U)) ↔ Continuous (boolIndicator (Subtype.val ⁻¹' U))
α : Type u
β : Type v
ι : Type ?u.179439
π : ι → Type ?u.179444
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ ContinuousOn (boolIndicator U) s ↔ IsClopen (Subtype.val ⁻¹' U)
rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_clopen]
no goals
α : Type u
β : Type v
ι : Type ?u.179439
π : ι → Type ?u.179444
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ Continuous (restrict s (boolIndicator U)) ↔ Continuous (boolIndicator (Subtype.val ⁻¹' U))
rfl