filter_univ_mem

Mathlib.Data.Finset.BooleanAlgebra

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

English

For any Finset s of α, filtering the universe by membership in s yields s: univ.filter (· ∈ s) = s.

Русский

Для любой финсет s над α фильтрование вселенной по принадлежности к s даёт s: univ.filter (x ∈ s) = s.

LaTeX

$$$\operatorname{univ}.filter (\\cdot \in s) = s$$$

Lean4

@[simp]
theorem filter_univ_mem (s : Finset α) : univ.filter (· ∈ s) = s := by simp [filter_mem_eq_inter]

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

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

Разделы

Аффилиация

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