toDFinsupp_inter

Mathlib.Data.DFinsupp.Multiset

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

English

toDFinsupp(s ∩ t) equals toDFinsupp s ⊓ toDFinsupp t.

Русский

toDFinsupp(s ∩ t) равно toDFinsupp s ⊓ toDFinsupp t.

LaTeX

$$$$ \\operatorname{toDFinsupp}(s \\cap t) = \\operatorname{toDFinsupp}(s) \\sqcap \\operatorname{toDFinsupp}(t) $$$$

Lean4

@[simp]
theorem toDFinsupp_inter (s t : Multiset α) : toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t := by ext i; simp

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

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

Разделы

Аффилиация

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