connectedComponentIn_nonempty_iff

English

The connectedComponentIn F x is nonempty if and only if x ∈ F.

Русский

Связанная компонента x в F непустая тогда и только тогда, когда x ∈ F.

LaTeX

$$$(connectedComponentIn F x).Nonempty \iff x \in F$$$

Lean4

theorem connectedComponentIn_nonempty_iff {x : α} {F : Set α} : (connectedComponentIn F x).Nonempty ↔ x ∈ F :=
  by
  rw [connectedComponentIn]
  split_ifs <;> simp [connectedComponent_nonempty, *]

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