mem_sep_iff

Mathlib.Data.Set.Basic

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

English

Two sub-collections {x ∈ s | p x} and {x ∈ s | q x} are equal iff ∀ x ∈ s, p x ↔ q x.

Русский

Два множества вида {x ∈ s | p x} и {x ∈ s | q x} равны тогда и только тогда, когда ∀ x ∈ s, p x ↔ q x.

LaTeX

$$$\{x \in s \mid p x\} = \{x \in s \mid q x\} \iff \forall x \in s, p x \iff q x$$$

Lean4

@[simp]
theorem mem_sep_iff : x ∈ {x ∈ s | p x} ↔ x ∈ s ∧ p x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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