sep_mem_eq

Mathlib.Data.Set.Basic

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

English

For sets s and t and predicate p, the set {x ∈ s | p x} equals s ∩ t when p is the membership in t.

Русский

Для множеств S и T и предиката P множество {x ∈ S | P(x)} равно S ∩ T при условии P(x) эквивалентно x ∈ T.

LaTeX

$$$\{x \in s \mid x \in t\} = s \cap t$$$

Lean4

@[simp]
theorem sep_mem_eq : {x ∈ s | x ∈ t} = s ∩ t :=
  rfl

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

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

Разделы

Аффилиация

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