lt_iff

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#IsAtom.lt_iff

English

For an atom a, x < a iff x = ⊥.

Русский

Для атома a, x < a эквивалентно x = ⊥.

LaTeX

$$$x < a \\iff x = \\bot.$$$

Lean4

theorem lt_iff (h : IsAtom a) : x < a ↔ x = ⊥ :=
  ⟨h.2 x, fun hx => hx.symm ▸ h.1.bot_lt⟩

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

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

Разделы

Аффилиация

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