case inl
α : Type u
β : Type v
ι : Type ?u.2516
π : ι → Type ?u.2521
inst✝ : TopologicalSpace α
s t u v : Set α
H : ∀ (x : α), x ∈ ∅ → ∀ (y : α), y ∈ ∅ → ∃ t, t ⊆ ∅ ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

case inr.intro
α : Type u
β : Type v
ι : Type ?u.2516
π : ι → Type ?u.2521
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s
α : Type u
β : Type v
ι : Type ?u.2516
π : ι → Type ?u.2521
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s
rcases eq_empty_or_nonempty s with (rfl | ⟨x, hx⟩)
no goals
case inl
α : Type u
β : Type v
ι : Type ?u.2516
π : ι → Type ?u.2521
inst✝ : TopologicalSpace α
s t u v : Set α
H : ∀ (x : α), x ∈ ∅ → ∀ (y : α), y ∈ ∅ → ∃ t, t ⊆ ∅ ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

case inr.intro
α : Type u
β : Type v
ι : Type ?u.2516
π : ι → Type ?u.2521
inst✝ : TopologicalSpace α
s✝ t u v s : Set α
H : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ t, t ⊆ s ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s
exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]