ofLex_inj

Mathlib.Order.Synonym

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

English

The map a ↦ ofLex a is injective from Lex α to α; equivalently, ofLex a = ofLex b implies a = b.

Русский

Отображение a ↦ ofLex a инъективно из Lex α в α; эквивалентно: ofLex a = ofLex b → a=b.

LaTeX

$$$\forall a,b:\, ofLex\,a = ofLex\,b \Rightarrow a=b$$$

Lean4

theorem ofLex_inj {a b : Lex α} : ofLex a = ofLex b ↔ a = b := by simp

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

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

Разделы

Аффилиация

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