lattice

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.lattice

English

The real numbers form a lattice: for any a,b ∈ ℝ both a ⊔ b and a ⊓ b exist.

Русский

Действительные образуют решётку: для любых a,b ∈ ℝ существуют их пределы верх и низ.

LaTeX

$$$\forall a,b \in \mathbb{R}, \; a \sqcup b, a \sqcap b \text{ exist}$$$

Lean4

instance lattice : Lattice ℝ :=
  inferInstance

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

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

Разделы

Аффилиация

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