case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s
rintro u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
⊢ Set.Nonempty (s ∩ (u ∩ v))
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
have xs : x ∈ s := by
  rcases H y ys with ⟨t, ts, xt, -, -⟩
  exact ts xt
case intro.intro.intro.intro.inl
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))

case intro.intro.intro.intro.inr
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
⊢ Set.Nonempty (s ∩ (u ∩ v))
cases hs xs
case intro.intro.intro.intro.inr
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case intro.intro.intro.intro.inl
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))

case intro.intro.intro.intro.inr
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case inl xu =>
  rcases H y ys with ⟨t, ts, xt, yt, ht⟩
  have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
  exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
no goals
case intro.intro.intro.intro.inr
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
h✝ : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
case inr xv =>
  rcases H z zs with ⟨t, ts, xt, zt, ht⟩
  have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
  exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
⊢ x ∈ s
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ x ∈ s
rcases H y ys with ⟨t, ts, xt, -, -⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
⊢ x ∈ s
exact ts xt
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
⊢ Set.Nonempty (s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
⊢ Set.Nonempty (s ∩ (u ∩ v))
rcases H y ys with ⟨t, ts, xt, yt, ht⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
this : Set.Nonempty (t ∩ (u ∩ v))
⊢ Set.Nonempty (s ∩ (u ∩ v))
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
⊢ Set.Nonempty (s ∩ (u ∩ v))
have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
t : Set α
ts : t ⊆ s
xt : x ∈ t
yt : y ∈ t
ht : IsPreconnected t
this : Set.Nonempty (t ∩ (u ∩ v))
⊢ Set.Nonempty (s ∩ (u ∩ v))
exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ Set.Nonempty (s ∩ (u ∩ v))
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
⊢ Set.Nonempty (s ∩ (u ∩ v))
rcases H z zs with ⟨t, ts, xt, zt, ht⟩
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
this : Set.Nonempty (t ∩ (v ∩ u))
⊢ Set.Nonempty (s ∩ (u ∩ v))
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ Set.Nonempty (s ∩ (u ∩ v))
have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
no goals
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
this : Set.Nonempty (t ∩ (v ∩ u))
⊢ Set.Nonempty (s ∩ (u ∩ v))
exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩
no goals
α : Type u
β : Type v
ι : Type ?u.1489
π : ι → Type ?u.1494
inst✝ : TopologicalSpace α
s✝ t✝ u✝ v✝ s : Set α
x : α
H : ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xv : x ∈ v
t : Set α
ts : t ⊆ s
xt : x ∈ t
zt : z ∈ t
ht : IsPreconnected t
⊢ s ⊆ v ∪ u
rwa [union_comm]