α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ Set.Nonempty (pi univ s) → (IsPreconnected (pi univ s) ↔ ∀ (x : ι), IsPreconnected (s x))
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ IsConnected (pi univ s) ↔ ∀ (i : ι), IsConnected (s i)
simp only [IsConnected, ← univ_pi_nonempty_iff, forall_and, and_congr_right_iff]
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : Set.Nonempty (pi univ s)
hc : IsPreconnected (pi univ s)
i : ι
⊢ IsPreconnected (s i)
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
⊢ Set.Nonempty (pi univ s) → (IsPreconnected (pi univ s) ↔ ∀ (x : ι), IsPreconnected (s x))
refine' fun hne => ⟨fun hc i => _, isPreconnected_univ_pi⟩
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : Set.Nonempty (pi univ s)
hc : IsPreconnected (pi univ s)
i : ι
⊢ IsPreconnected ((fun f => f i) '' pi univ s)
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : Set.Nonempty (pi univ s)
hc : IsPreconnected (pi univ s)
i : ι
⊢ IsPreconnected (s i)
rw [← eval_image_univ_pi hne]
no goals
α : Type u
β : Type v
ι : Type u_2
π : ι → Type u_1
inst✝¹ : TopologicalSpace α
s✝ t u v : Set α
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hne : Set.Nonempty (pi univ s)
hc : IsPreconnected (pi univ s)
i : ι
⊢ IsPreconnected ((fun f => f i) '' pi univ s)
exact hc.image _ (continuous_apply _).continuousOn