case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous (boolIndicator U) → IsClopen U

case mpr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ IsClopen U → Continuous (boolIndicator U)
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous (boolIndicator U) ↔ IsClopen U
constructor
case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hc : Continuous (boolIndicator U)
⊢ IsClopen U
case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous (boolIndicator U) → IsClopen U
intro hc
case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hc : Continuous (boolIndicator U)
⊢ IsClopen (boolIndicator U ⁻¹' {true})
case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hc : Continuous (boolIndicator U)
⊢ IsClopen U
rw [← U.preimage_boolIndicator_true]
no goals
case mp
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hc : Continuous (boolIndicator U)
⊢ IsClopen (boolIndicator U ⁻¹' {true})
exact ⟨(isOpen_discrete _).preimage hc, (isClosed_discrete _).preimage hc⟩
case mpr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
⊢ IsOpen (boolIndicator U ⁻¹' s)
case mpr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ IsClopen U → Continuous (boolIndicator U)
refine' fun hU => ⟨fun s _ => _⟩
case mpr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = univ
⊢ IsOpen univ

case mpr.inr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = U
⊢ IsOpen U

case mpr.inr.inr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = Uᶜ
⊢ IsOpen (Uᶜ)

case mpr.inr.inr.inr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = ∅
⊢ IsOpen ∅
case mpr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
⊢ IsOpen (boolIndicator U ⁻¹' s)
rcases U.preimage_boolIndicator s with (h | h | h | h) <;> rw [h]
no goals
case mpr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = univ
⊢ IsOpen univ

case mpr.inr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = U
⊢ IsOpen U

case mpr.inr.inr.inl
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = Uᶜ
⊢ IsOpen (Uᶜ)

case mpr.inr.inr.inr
α : Type u
β : Type v
ι : Type ?u.178896
π : ι → Type ?u.178901
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s✝ t : Set α
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
hU : IsClopen U
s : Set Bool
x✝ : IsOpen s
h : boolIndicator U ⁻¹' s = ∅
⊢ IsOpen ∅
exacts [isOpen_univ, hU.1, hU.2.isOpen_compl, isOpen_empty]