right_eq_sup

Mathlib.Order.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem right_eq_sup : b = a ⊔ b ↔ a ≤ b :=
  eq_comm.trans sup_eq_right

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

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

Разделы

Аффилиация

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