cons_same

Mathlib.Data.Multiset.Pi

URI: https://scilib.ai/kg/mathlib#Multiset.Pi.cons_same

Lean4

theorem cons_same {b : δ a} {f : ∀ a ∈ m, δ a} (h : a ∈ a ::ₘ m) : cons m a b f a h = b :=
  dif_pos rfl

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

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

Разделы

Аффилиация

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