toScott_ofScott

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithScott.toScott_ofScott

English

For any a in WithScott α, applying ofScott then toScott leaves a unchanged.

Русский

Для любого a ∈ WithScott α применение ofScott затем toScott оставляет a без изменений.

LaTeX

$$$\mathrm{toScott}(\mathrm{ofScott}(a)) = a.$$$

Lean4

@[simp]
theorem toScott_ofScott (a : WithScott α) : toScott (ofScott a) = a :=
  rfl

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

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

Разделы

Аффилиация

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