ordConnectedComponent_eq — Mathlib

English

If the order-interval between x and y is contained in s, then the order-connected components containing x and y are equal: if [[x,y]] ⊆ s, then ordConnectedComponent(s,x) = ordConnectedComponent(s,y).

Русский

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

LaTeX

$$$[[x, y]] \subseteq s \Rightarrow \operatorname{ordConnectedComponent}(s, x) = \operatorname{ordConnectedComponent}(s, y)$$$

Lean4

theorem ordConnectedComponent_eq (h : [[x, y]] ⊆ s) : ordConnectedComponent s x = ordConnectedComponent s y :=
  ext fun _ => ⟨mem_ordConnectedComponent_trans (mem_ordConnectedComponent_comm.2 h), mem_ordConnectedComponent_trans h⟩

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