mem_ordConnectedComponent_comm — Mathlib

English

Membership in an order-connected component is symmetric: y ∈ ordConnectedComponent(s, x) iff x ∈ ordConnectedComponent(s, y).

Русский

Принадлежность к ор connected-компоненте симметрична: y ∈ ordConnectedComponent(s, x) ⇔ x ∈ ordConnectedComponent(s, y).

LaTeX

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

Lean4

theorem mem_ordConnectedComponent_comm : y ∈ ordConnectedComponent s x ↔ x ∈ ordConnectedComponent s y := by
  rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]

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