le_inf

Mathlib.Order.Lattice

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

English

If a ≤ b and a ≤ c, then a ≤ b ⊓ c.

Русский

Если a ≤ b и a ≤ c, то a ≤ b ⊓ c.

LaTeX

$$$ a \le b \quad \text{and} \quad a \le c \;\Rightarrow\; a \le b \sqcap c $$$

Lean4

theorem le_inf : a ≤ b → a ≤ c → a ≤ b ⊓ c :=
  SemilatticeInf.le_inf a b c

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

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

Разделы

Аффилиация

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