left_eq_sup

Mathlib.Order.Lattice

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

English

a = a ⊔ b if and only if b ≤ a.

Русский

a = a ⊔ b тогда и только тогда, когда b ≤ a.

LaTeX

$$$a = a \\lor b \\iff b \\le a$$$

Lean4

@[simp]
theorem left_eq_sup : a = a ⊔ b ↔ b ≤ a :=
  eq_comm.trans sup_eq_left

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

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

Разделы

Аффилиация

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