α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
⊢ ∀ (u v : Set α),
    IsOpen u → IsOpen v → s ⊆ u ∪ v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
⊢ IsPreconnected s
unfold IsPreconnected
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
this :
  ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∪ v ∧ Set.Nonempty (s ∩ u) ∧ Set.Nonempty (s ∩ v) ∧ ¬Set.Nonempty (s ∩ (u ∩ v))
⊢ False
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
⊢ ∀ (u v : Set α),
    IsOpen u → IsOpen v → s ⊆ u ∪ v → Set.Nonempty (s ∩ u) → Set.Nonempty (s ∩ v) → Set.Nonempty (s ∩ (u ∩ v))
by_contra'
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : ¬Set.Nonempty (s ∩ (u ∩ v))
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
this :
  ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∪ v ∧ Set.Nonempty (s ∩ u) ∧ Set.Nonempty (s ∩ v) ∧ ¬Set.Nonempty (s ∩ (u ∩ v))
⊢ False
rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : ¬Set.Nonempty (s ∩ (u ∩ v))
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False
rw [not_nonempty_iff_eq_empty] at H
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
⊢ False
have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_not_mem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
this : ContinuousOn (boolIndicator u) s
⊢ False
simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.not_mem_iff_boolIndicator _).mp hy] using
  hs _ this x x_in_s y y_in_s
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsOpen (Subtype.val ⁻¹' u)

α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsClosed (Subtype.val ⁻¹' u)
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ ContinuousOn (boolIndicator u) s
apply (continuousOn_boolIndicator_iff_clopen _ _).mpr ⟨_, _⟩
no goals
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsOpen (Subtype.val ⁻¹' u)
exact u_op.preimage continuous_subtype_val
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsClosed ((Subtype.val ⁻¹' v)ᶜ)
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsClosed (Subtype.val ⁻¹' u)
rw [preimage_subtype_coe_eq_compl hsuv H]
no goals
α : Type u
β : Type v
ι : Type ?u.145858
π : ι → Type ?u.145863
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x = f y
u v : Set α
u_op : IsOpen u
v_op : IsOpen v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : ¬y ∈ u
⊢ IsClosed ((Subtype.val ⁻¹' v)ᶜ)
exact (v_op.preimage continuous_subtype_val).isClosed_compl