ordSeparatingSet_comm — Mathlib

English

Defining ordSeparatingSet(s,t) as the intersection of the union over s of ordConnectedComponent(tᶜ x) and the union over t of ordConnectedComponent(sᶜ x). It captures points lying between s and t endpoints in different components.

Русский

Определение ordSeparatingSet(s,t) как пересечение объединений ordConnectedComponent(tᶜ x) и ordConnectedComponent(sᶜ x) по соответствующим x из s и t.

LaTeX

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

Lean4

theorem ordSeparatingSet_comm (s t : Set α) : ordSeparatingSet s t = ordSeparatingSet t s :=
  inter_comm _ _

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