α : Type u
β : Type v
ι : Type ?u.2906
π : ι → Type ?u.2911
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
c : Set (Set α)
H1 : ∀ (s : Set α), s ∈ c → x ∈ s
H2 : ∀ (s : Set α), s ∈ c → IsPreconnected s
⊢ ∀ (y : α), y ∈ ⋃₀ c → ∃ t, t ⊆ ⋃₀ c ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
α : Type u
β : Type v
ι : Type ?u.2906
π : ι → Type ?u.2911
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
c : Set (Set α)
H1 : ∀ (s : Set α), s ∈ c → x ∈ s
H2 : ∀ (s : Set α), s ∈ c → IsPreconnected s
⊢ IsPreconnected (⋃₀ c)
apply isPreconnected_of_forall x
case intro.intro
α : Type u
β : Type v
ι : Type ?u.2906
π : ι → Type ?u.2911
inst✝ : TopologicalSpace α
s✝ t u v : Set α
x : α
c : Set (Set α)
H1 : ∀ (s : Set α), s ∈ c → x ∈ s
H2 : ∀ (s : Set α), s ∈ c → IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t, t ⊆ ⋃₀ c ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
α : Type u
β : Type v
ι : Type ?u.2906
π : ι → Type ?u.2911
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
c : Set (Set α)
H1 : ∀ (s : Set α), s ∈ c → x ∈ s
H2 : ∀ (s : Set α), s ∈ c → IsPreconnected s
⊢ ∀ (y : α), y ∈ ⋃₀ c → ∃ t, t ⊆ ⋃₀ c ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
rintro y ⟨s, sc, ys⟩
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.2906
π : ι → Type ?u.2911
inst✝ : TopologicalSpace α
s✝ t u v : Set α
x : α
c : Set (Set α)
H1 : ∀ (s : Set α), s ∈ c → x ∈ s
H2 : ∀ (s : Set α), s ∈ c → IsPreconnected s
y : α
s : Set α
sc : s ∈ c
ys : y ∈ s
⊢ ∃ t, t ⊆ ⋃₀ c ∧ x ∈ t ∧ y ∈ t ∧ IsPreconnected t
exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩