setOf_injective

Mathlib.Data.Set.Basic

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

English

The map setOf: (α → Prop) → Set α is injective, i.e., if setOf p = setOf q then p = q.

Русский

Отображение setOf: (α → Prop) → Set α инъективно: если setOf p = setOf q, то p = q.

LaTeX

$$$\text{Injective}(\text{setOf})\;:\; (p,q: α \to Prop) \;\mapsto\; {x \mid p(x)} = {x \mid q(x)} \Rightarrow p = q$$$

Lean4

theorem setOf_injective : Function.Injective (@setOf α) :=
  injective_id

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

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

Разделы

Аффилиация

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