inf_le_left

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.inf_le_left

English

The infimum a ⊓ b is less than or equal to a.

Русский

Наименьшее-верхняя граница: a ⊓ b ≤ a.

LaTeX

$$$\forall a,b \in \mathrm{CauSeq}(\alpha, \mathrm{abs})\; (a \wedge b) \le a$$$

Lean4

protected theorem inf_le_left {a b : CauSeq α abs} : a ⊓ b ≤ a :=
  le_of_exists ⟨0, fun _ _ => inf_le_left⟩

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

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

Разделы

Аффилиация

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