specializes_iff_le

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsUpperSet.specializes_iff_le

English

In the upper-set topology, a specializes to b iff b ≤ a.

Русский

В топологии верхних множеств a специализируется на b тогда, когда b ≤ a.

LaTeX

$$$ a \;\triangleright\; b \iff b \le a. $$$

Lean4

theorem specializes_iff_le {a b : α} : a ⤳ b ↔ b ≤ a := by
  simp only [specializes_iff_closure_subset, closure_singleton, Iic_subset_Iic]

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

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

Разделы

Аффилиация

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