α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
⊢ s ⊆ connectedComponentIn F x
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ s ⊆ connectedComponentIn F x
have : IsPreconnected (((↑) : F → α) ⁻¹' s) := by
  refine' inducing_subtype_val.isPreconnected_image.mp _
  rwa [Subtype.image_preimage_coe, inter_eq_left_iff_subset.mpr hsF]
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
⊢ s ⊆ connectedComponentIn F x
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
⊢ s ⊆ connectedComponentIn F x
have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
  rw [mem_preimage]
  exact hxs
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ connectedComponentIn F x
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
⊢ s ⊆ connectedComponentIn F x
have := this.subset_connectedComponent h2xs
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ Subtype.val '' connectedComponent { val := x, property := (_ : x ∈ F) }
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ connectedComponentIn F x
rw [connectedComponentIn_eq_image (hsF hxs)]
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ Subtype.val '' (Subtype.val ⁻¹' s)
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ Subtype.val '' connectedComponent { val := x, property := (_ : x ∈ F) }
refine' Subset.trans _ (image_subset _ this)
no goals
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this✝ : IsPreconnected (Subtype.val ⁻¹' s)
h2xs : { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
this : Subtype.val ⁻¹' s ⊆ connectedComponent { val := x, property := (_ : x ∈ F) }
⊢ s ⊆ Subtype.val '' (Subtype.val ⁻¹' s)
rw [Subtype.image_preimage_coe, inter_eq_left_iff_subset.mpr hsF]
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val '' (Subtype.val ⁻¹' s))
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val ⁻¹' s)
refine' inducing_subtype_val.isPreconnected_image.mp _
no goals
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
⊢ IsPreconnected (Subtype.val '' (Subtype.val ⁻¹' s))
rwa [Subtype.image_preimage_coe, inter_eq_left_iff_subset.mpr hsF]
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
⊢ ↑{ val := x, property := (_ : x ∈ F) } ∈ s
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
⊢ { val := x, property := (_ : x ∈ F) } ∈ Subtype.val ⁻¹' s
rw [mem_preimage]
no goals
α : Type u
β : Type v
ι : Type ?u.54741
π : ι → Type ?u.54746
inst✝ : TopologicalSpace α
s t u v : Set α
x : α
F : Set α
hs : IsPreconnected s
hxs : x ∈ s
hsF : s ⊆ F
this : IsPreconnected (Subtype.val ⁻¹' s)
⊢ ↑{ val := x, property := (_ : x ∈ F) } ∈ s
exact hxs