setOf_inj

Mathlib.Data.Set.Basic

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

English

Another formulation asserting that equality of setOf predicates implies equality of predicates.

Русский

Другая формулировка утверждает, что равенство множеств вида setOf по предикатам влечет равенство самих предикатов.

LaTeX

$$$\{x \mid p x\} = \{x \mid q x\} \iff p = q$$$

Lean4

theorem setOf_inj {p q : α → Prop} : {x | p x} = {x | q x} ↔ p = q :=
  Iff.rfl

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

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

Разделы

Аффилиация

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