insert_inter_distrib

Mathlib.Data.Finset.Basic

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

English

Inserting into an intersection distributes: insert a (s ∩ t) = insert a s ∩ insert a t.

Русский

Вставка в пересечение распределяется: insert a (s ∩ t) = insert a s ∩ insert a t.

LaTeX

$$$ insert\\ a\\ (s \\cap t) = insert\\ a\\ s \\cap insert\\ a\\ t $$$

Lean4

theorem insert_inter_distrib (s t : Finset α) (a : α) : insert a (s ∩ t) = insert a s ∩ insert a t := by grind

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

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

Разделы

Аффилиация

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