right_eq_inf

Mathlib.Order.Lattice

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

English

b = a ⊓ b iff b ≤ a.

Русский

b = a ⊓ b эквивалентно b ≤ a.

LaTeX

$$$ b = a \sqcap b \iff b \le a $$$

Lean4

@[simp]
theorem right_eq_inf : b = a ⊓ b ↔ b ≤ a :=
  eq_comm.trans inf_eq_right

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

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

Разделы

Аффилиация

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