setOf_inter_eq_sep

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.setOf_inter_eq_sep

English

The intersection with setOf gives the same as the setOf of membership in the set.

Русский

Пересечение с множестов-setOf эквивалентно множеству элементов множества, входящих в setOf.

LaTeX

$$s ∩ {a \mid p a} = {a \in s \mid p a}$$

Lean4

theorem setOf_inter_eq_sep (p : α → Prop) (s : Set α) : {a | p a} ∩ s = {a ∈ s | p a} :=
  inter_comm _ _

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

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

Разделы

Аффилиация

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