pimage_union

Mathlib.Data.Finset.PImage

URI: https://scilib.ai/kg/mathlib#Finset.pimage_union

← MathLib Explorer

English

Pimage distributes over finite unions: (s ∪ t).pimage f = s.pimage f ∪ t.pimage f.

Русский

Pimage распределяется по объединению: (s ∪ t).pimage f = s.pimage f ∪ t.pimage f.

LaTeX

$$$ (s \cup t).pimage f = s.pimage f \cup t.pimage f $.$$

Lean4

theorem pimage_union [DecidableEq α] : (s ∪ t).pimage f = s.pimage f ∪ t.pimage f :=
  coe_inj.1 <| by simp only [coe_pimage, coe_union, ← PFun.image_union]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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