no goals
α : Type u
β : Type v
ι : Type ?u.3583
π : ι → Type ?u.3588
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ (s_1 : Set α), s_1 ∈ {s, t} → x ∈ s_1
rintro r (rfl | rfl | h) <;> assumption
no goals
α : Type u
β : Type v
ι : Type ?u.3583
π : ι → Type ?u.3588
inst✝ : TopologicalSpace α
s✝ t✝ u v : Set α
x : α
s t : Set α
H1 : x ∈ s
H2 : x ∈ t
H3 : IsPreconnected s
H4 : IsPreconnected t
⊢ ∀ (s_1 : Set α), s_1 ∈ {s, t} → IsPreconnected s_1
rintro r (rfl | rfl | h) <;> assumption