inf_singleton

Mathlib.Data.Multiset.Lattice

URI: https://scilib.ai/kg/mathlib#Multiset.inf_singleton

English

The infimum of a singleton {a} is a: inf({a}) = a.

Русский

Наименьшая грань одиночного множества {a} равна a.

LaTeX

$$$$ ({a}:\\mathrm{Multiset})(\\alpha)).inf = a $$$$

Lean4

@[simp]
theorem inf_singleton {a : α} : ({ a } : Multiset α).inf = a :=
  inf_top_eq _

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

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

Разделы

Аффилиация

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