inter_filter

Mathlib.Data.Finset.Basic

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

English

Let S and T be finite sets and P a predicate on α. Then S ∩ { x ∈ T | P(x) } = { x ∈ S ∩ T | P(x) }.

Русский

Пусть S и T — конечные множества, а P — предикат на α. Тогда S ∩ { x ∈ T | P(x) } = { x ∈ S ∩ T | P(x) }.

LaTeX

$$$S \\cap \\operatorname{filter}_p(T) = \\operatorname{filter}_p(S \\cap T)$$$

Lean4

theorem inter_filter (s t : Finset α) : s ∩ filter p t = filter p (s ∩ t) := by grind

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

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

Разделы

Аффилиация

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