ordConnectedComponent_eq_empty — Mathlib

English

Let α be a linearly ordered set and s ⊆ α. For any x ∈ α, the order-connected component of s containing x is empty if and only if x ∉ s.

Русский

Пусть α — линейно упорядоченное множество и s ⊆ α. Для любого x ∈ α ор connected-компонента s, содержащая x, пуста тогда и только тогда, когда x ∉ s.

LaTeX

$$$\operatorname{ordConnectedComponent}(s, x) = \emptyset \iff x \notin s$$$

Lean4

@[simp]
theorem ordConnectedComponent_eq_empty : ordConnectedComponent s x = ∅ ↔ x ∉ s := by
  rw [← not_nonempty_iff_eq_empty, nonempty_ordConnectedComponent]

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