mem_ordConnectedComponent — Mathlib

English

y belongs to the ord-connected component of x in s if and only if [[x,y]] ⊆ s.

Русский

y принадлежит ородостоиновому компоненту x в s тогда и только тогда, когда [[x,y]] ⊆ s.

LaTeX

$$$\\text{mem\_ordConnectedComponent}:\\ y \\in \\operatorname{ordConnectedComponent}(s,x) \\iff [[x,y]] \\subseteq s$$$

Lean4

theorem mem_ordConnectedComponent : y ∈ ordConnectedComponent s x ↔ [[x, y]] ⊆ s :=
  Iff.rfl

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