ordConnectedSection — Mathlib

English

ordConnectedSection(s) is defined as the range of ordConnectedProj(s); i.e., it picks one representative from each order-connected component of s.

Русский

ordConnectedSection(s) определяется как диапазон ordConnectedProj(s); то есть выбирается по одному представителю из каждой компонентной компоненты порядка множества s.

LaTeX

$$$\operatorname{ordConnectedSection}(s) = \operatorname{range}(\operatorname{ordConnectedProj}(s))$$$

Lean4

/-- A set that intersects each order connected component of a set by a single point. Defined as the
range of `Set.ordConnectedProj s`. -/
def ordConnectedSection (s : Set α) : Set α :=
  range <| ordConnectedProj s

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