mem_connectedComponentIn — Mathlib

English

Let F be a subset of α and x ∈ α. If hx holds that x ∈ F, then x lies in the connected component of x in F.

Русский

Пусть F ⊆ α и x ∈ α. Если x ∈ F, то x принадлежит связной компоненте x внутри F.

LaTeX

$$$x \in F \Rightarrow x \in \operatorname{connectedComponentIn} F x$$$

Lean4

theorem mem_connectedComponentIn {x : α} {F : Set α} (hx : x ∈ F) : x ∈ connectedComponentIn F x := by
  simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]

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