ordConnectedComponent_ordConnectedProj

English

For x ∈ s, ordConnectedComponent(s, ordConnectedProj(s)(x)) equals ordConnectedComponent(s, x).

Русский

Для x ∈ s компонент ordConnectedComponent(s, ordConnectedProj(s)(x)) совпадает с ordConnectedComponent(s, x).

LaTeX

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

Lean4

@[simp]
theorem ordConnectedComponent_ordConnectedProj (s : Set α) (x : s) :
    ordConnectedComponent s (ordConnectedProj s x) = ordConnectedComponent s x :=
  ordConnectedComponent_eq <| mem_ordConnectedComponent_ordConnectedProj _ _

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