mem_bind

Mathlib.Data.Multiset.Bind

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

English

An element b belongs to bind s f iff there exists a ∈ s with b ∈ f a.

Русский

Элемент b принадлежит bind s f тогда и только тогда, когда существует a ∈ s такое, что b ∈ f a.

LaTeX

$$$b \\in bind\\, s\\, f \\iff \\exists a \\in s,\\; b \\in f a$$$

Lean4

@[simp]
theorem mem_bind {b s} {f : α → Multiset β} : b ∈ bind s f ↔ ∃ a ∈ s, b ∈ f a := by simp [bind]

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

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

Разделы

Аффилиация

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