subset_connectedComponentIn — Mathlib

English

If s is preconnected and x ∈ s and s ⊆ F, then s ⊆ connectedComponentIn F x.

Русский

Если s предсвязно, x ∈ s и s ⊆ F, то s ⊆ connectedComponentIn F x.

LaTeX

$$$s \subseteq connectedComponentIn F x$$$

Lean4

theorem subset_connectedComponentIn {x : α} {F : Set α} (hs : IsPreconnected s) (hxs : x ∈ s) (hsF : s ⊆ F) :
    s ⊆ connectedComponentIn F x :=
  by
  have : IsPreconnected (((↑) : F → α) ⁻¹' s) :=
    by
    refine IsInducing.subtypeVal.isPreconnected_image.mp ?_
    rwa [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]
  have h2xs : (⟨x, hsF hxs⟩ : F) ∈ (↑) ⁻¹' s := by
    rw [mem_preimage]
    exact hxs
  have := this.subset_connectedComponent h2xs
  rw [connectedComponentIn_eq_image (hsF hxs)]
  refine Subset.trans ?_ (image_mono this)
  rw [Subtype.image_preimage_coe, inter_eq_right.mpr hsF]

Похожие утверждения