α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ f x = f y
α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
⊢ f x = f y
let F : S → T := hTm.restrict f S T
α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ F { val := x, property := hx } = F { val := y, property := hy }
α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ f x = f y
suffices F ⟨x, hx⟩ = F ⟨y, hy⟩ by rwa [← Subtype.coe_inj] at this
no goals
α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
⊢ F { val := x, property := hx } = F { val := y, property := hy }
exact (isPreconnected_iff_preconnectedSpace.mp hS).constant (hc.restrict_mapsTo _)
no goals
α : Type u
β : Type v
ι : Type ?u.149420
π : ι → Type ?u.149425
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : TopologicalSpace β
S : Set α
hS : IsPreconnected S
T : Set β
inst✝ : DiscreteTopology ↑T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
x y : α
hx : x ∈ S
hy : y ∈ S
F : ↑S → ↑T := MapsTo.restrict f S T hTm
this : F { val := x, property := hx } = F { val := y, property := hy }
⊢ f x = f y
rwa [← Subtype.coe_inj] at this