K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
⊢ EqOn f 1 S ∨ EqOn f (-1) S
have : DiscreteTopology ({1, -1} : Set 𝕜) := discrete_of_t1_of_finite
case hmaps
K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ MapsTo f S {1, -1}

K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
have hmaps : MapsTo f S {1, -1}
no goals
K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
hmaps : MapsTo f S {1, -1}
⊢ EqOn f 1 S ∨ EqOn f (-1) S
simpa using hS.eqOn_const_of_mapsTo hf hmaps
no goals
case hmaps
K : Type ?u.15846
inst✝⁶ : DivisionRing K
inst✝⁵ : TopologicalSpace K
α : Type u_2
𝕜 : Type u_1
f g : α → 𝕜
S : Set α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace 𝕜
inst✝² : T1Space 𝕜
inst✝¹ : Ring 𝕜
inst✝ : NoZeroDivisors 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hsq : EqOn (f ^ 2) 1 S
this : DiscreteTopology ↑{1, -1}
⊢ MapsTo f S {1, -1}
simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq