mem_ordConnectedComponent_trans — Mathlib

English

If y lies in the component of x (within s) and z lies in the component of y (within s), then z lies in the component of x (within s).

Русский

Если y принадлежит компоненте x в s, а z принадлежит компоненте y в s, то z принадлежит компоненте x в s.

LaTeX

$$$\,y \in \operatorname{ordConnectedComponent}(s, x) \to z \in \operatorname{ordConnectedComponent}(s, y) \to z \in \operatorname{ordConnectedComponent}(s, x)$$$

Lean4

theorem mem_ordConnectedComponent_trans (hxy : y ∈ ordConnectedComponent s x) (hyz : z ∈ ordConnectedComponent s y) :
    z ∈ ordConnectedComponent s x :=
  calc
    [[x, z]] ⊆ [[x, y]] ∪ [[y, z]] := uIcc_subset_uIcc_union_uIcc
    _ ⊆ s := union_subset hxy hyz

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