mem_ordConnectedComponent_ordConnectedProj

English

For x ∈ s, the underlying element ↑x belongs to the component ordConnectedComponent(s, ordConnectedProj(s)(x)).

Русский

Пусть x ∈ s; принадлежащий ему элемент ↑x принадлежит ordConnectedComponent(s, ordConnectedProj(s)(x)).

LaTeX

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

Lean4

theorem mem_ordConnectedComponent_ordConnectedProj (s : Set α) (x : s) :
    ↑x ∈ ordConnectedComponent s (ordConnectedProj s x) :=
  mem_ordConnectedComponent_comm.2 <| ordConnectedProj_mem_ordConnectedComponent s x

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