X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y
let U := f ⁻¹' {f y}
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
this : ¬x ∈ Uᶜ
⊢ f x = f y

case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ f x = f y
suffices : x ∉ Uᶜ
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
this : ¬x ∈ Uᶜ
⊢ f x = f y

case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
exact Classical.not_not.1 this
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
⊢ ¬x ∈ Uᶜ
intro hxV
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ

case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : Set.Nonempty (s ∩ (U ∩ Uᶜ))
⊢ False
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ False
specialize hs U (Uᶜ) (hf {f y}) (hf ({f y}ᶜ)) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
no goals
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
⊢ s ⊆ U ∪ Uᶜ
simp only [union_compl_self, subset_univ]
no goals
case this
X : Type u_1
Y : Type u_2
Z : Type ?u.4691
α : Type ?u.4694
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
x y : X
hx : x ∈ s
hy : y ∈ s
U : Set X := f ⁻¹' {f y}
hxV : x ∈ Uᶜ
hs : Set.Nonempty (s ∩ (U ∩ Uᶜ))
⊢ False
simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs