nonempty_ordConnectedComponent

Mathlib.Order.Interval.Set.OrdConnectedComponent

URI: https://scilib.ai/kg/mathlib#Set.nonempty_ordConnectedComponent

← MathLib Explorer

English

The ord-connected component of x in s is nonempty if and only if x ∈ s.

Русский

ordConnectedComponent(s,x) непусто ⇔ x ∈ s.

LaTeX

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

Lean4

@[simp]
theorem nonempty_ordConnectedComponent : (ordConnectedComponent s x).Nonempty ↔ x ∈ s :=
  ⟨fun ⟨_, hy⟩ => hy <| left_mem_uIcc, fun h => ⟨x, self_mem_ordConnectedComponent.2 h⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru