bind_congr

Mathlib.Data.Multiset.Bind

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

English

If f a = g a for all a in m, then bind m f = bind m g.

Русский

Если для всех a ∈ m выполняется f a = g a, то bind m f = bind m g.

LaTeX

$$$(\\forall a \\in m, f a = g a) \\Rightarrow (m.bind f = m.bind g)$$$

Lean4

theorem bind_congr {f g : α → Multiset β} {m : Multiset α} : (∀ a ∈ m, f a = g a) → bind m f = bind m g := by
  simp +contextual [bind]

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

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

Разделы

Аффилиация

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