isClosed_le_prod

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#isClosed_le_prod

English

The set of pairs (x,y) with x ≤ y is closed in α × α whenever α is an ordered space with OrderClosedTopology.

Русский

Множество пар (x,y) с x ≤ y замкнуто в α × α при условии OrderClosedTopology на α.

LaTeX

$$$\text{IsClosed} \{ p \in α \times α \mid p_1 \le p_2 \}$$$

Lean4

theorem isClosed_le_prod : IsClosed {p : α × α | p.1 ≤ p.2} :=
  t.isClosed_le'

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

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

Разделы

Аффилиация

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