csInf_pair

Mathlib.Order.ConditionallyCompleteLattice.Basic

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

English

The infimum of two elements equals their lattice meet: sInf {a, b} = a ⊓ b.

Русский

Infimum двух элементов равен их пересечению: sInf {a, b} = a ⊓ b.

LaTeX

$$$\forall a,b:\\alpha,\ sInf\{a,b\} = a \sqcap b$$$

Lean4

theorem csInf_pair (a b : α) : sInf { a, b } = a ⊓ b :=
  (@isGLB_pair _ _ a b).csInf_eq (insert_nonempty _ _)

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

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

Разделы

Аффилиация

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