ordConnectedProj_mem_ordConnectedComponent

English

For every s and x ∈ s, the projection ordConnectedProj(s)(x) lies in ordConnectedComponent(s, x).

Русский

Для любого s и x ∈ s, образ ordConnectedProj(s)(x) принадлежит ordConnectedComponent(s, x).

LaTeX

$$$\operatorname{ordConnectedProj}(s)(x) \in \operatorname{ordConnectedComponent}(s, x)$$$

Lean4

theorem ordConnectedProj_mem_ordConnectedComponent (s : Set α) (x : s) :
    ordConnectedProj s x ∈ ordConnectedComponent s x :=
  Nonempty.some_mem _

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