inf_ndinsert

Mathlib.Data.Multiset.Lattice

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

← MathLib Explorer

English

Same as above: the infimum of ndinsert a s equals a ⊓ s.inf.

Русский

То же самое: inf(ndinsert a s) = a ∧ inf s.

LaTeX

$$$$ (\\mathrm{ndinsert}\\ a\\ s).inf = a \\inf s $$$$

Lean4

@[simp]
theorem inf_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).inf = a ⊓ s.inf := by
  rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_cons]; simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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