toLex_inj

Mathlib.Order.Synonym

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

English

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

Русский

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

LaTeX

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

Lean4

theorem toLex_inj {a b : α} : toLex a = toLex b ↔ a = b := by simp

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

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

Разделы

Аффилиация

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