inter_erase

Mathlib.Data.Finset.Basic

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

English

For any a, s, t, the intersection of s with t without a equals the erase of a from the intersection s ∩ t.

Русский

Для любого a, s, t: s ∩ (t \\ {a}) = (s ∩ t) \\ {a}.

LaTeX

$$$ \\forall a:\\alpha, \\forall s,t : Finset \\alpha, s \\cap (t \\{a\\}) = (s \\cap t) \\{a\\}$$$

Lean4

theorem inter_erase (a : α) (s t : Finset α) : s ∩ t.erase a = (s ∩ t).erase a := by grind

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

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

Разделы

Аффилиация

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