sup_bind

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.sup_bind

English

The bind distributes over supremum: bind (f ⊔ g) h = bind f h ⊔ bind g h.

Русский

Связывание распределяется по сходу: bind (f ⊔ g) h = bind f h ⊔ bind g h.

LaTeX

$$$\\mathrm{bind}(f \\sqcup g)\\, h = \\mathrm{bind}(f,h) \\sqcup \\mathrm{bind}(g,h)$$$

Lean4

theorem sup_bind {f g : Filter α} {h : α → Filter β} : bind (f ⊔ g) h = bind f h ⊔ bind g h :=
  rfl

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

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

Разделы

Аффилиация

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