ordT5Nhd — Mathlib

English

ordT5Nhd(s,t) is the union over x ∈ s of the order-connected components of tᶜ ∩ (ordConnectedSection(ordSeparatingSet s t))ᶜ, evaluated at x.

Русский

ordT5Nhd(s,t) — объединение по x ∈ s компонентordConnectedComponent( tᶜ ∩ (ordConnectedSection(ordSeparatingSet s t))ᶜ ) x.

LaTeX

$$ordT5Nhd(s,t) = ⋃ x ∈ s, ordConnectedComponent( t^c ∩ (ordConnectedSection( ordSeparatingSet s t))^c ) x$$

Lean4

/-- An auxiliary neighborhood that will be used in the proof of
`OrderTopology.CompletelyNormalSpace`. -/
def ordT5Nhd (s t : Set α) : Set α :=
  ⋃ x ∈ s, ordConnectedComponent (tᶜ ∩ (ordConnectedSection <| ordSeparatingSet s t)ᶜ) x

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