ofLowerSet_toLowerSet

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLowerSet.ofLowerSet_toLowerSet

English

The map toLowerSet is injective: toLowerSet(a) = toLowerSet(b) implies a = b.

Русский

Отображение toLowerSet инъективно: toLowerSet(a) = toLowerSet(b) → a = b.

LaTeX

$$$\forall {a,b:\alpha}:\; \mathrm{toLowerSet}(a) = \mathrm{toLowerSet}(b) \iff a = b$$$

Lean4

@[simp]
theorem ofLowerSet_toLowerSet (a : α) : ofLowerSet (toLowerSet a) = a :=
  rfl

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

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

Разделы

Аффилиация

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