toScott_inj

Mathlib.Topology.Order.ScottTopology

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

English

The map toScott is injective: toScott a = toScott b implies a = b.

Русский

Отображение toScott инъективно: из равенства toScott a = toScott b следует a = b.

LaTeX

$$$ toScott(a) = toScott(b) \iff a = b.$$$

Lean4

theorem toScott_inj {a b : α} : toScott a = toScott b ↔ a = b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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