connectedComponentIn_eq_image — Mathlib

English

If x ∈ F, then connectedComponentIn F x equals the image of the connected component of (x,h) in the subtype F.

Русский

Если x ∈ F, то connectedComponentIn F x равно образу связной компоненты (x,h) в подмножестве F.

LaTeX

$$$\\mathrm{connectedComponentIn}(F,x) = (\\uparrow)''\\mathrm{connectedComponent}(\\langle x,h\\rangle) \\quad (h:\\ x\\in F)$$$

Lean4

theorem connectedComponentIn_eq_image {F : Set α} {x : α} (h : x ∈ F) :
    connectedComponentIn F x = (↑) '' connectedComponent (⟨x, h⟩ : F) :=
  dif_pos h

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