singleton_injective

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.singleton_injective

← MathLib Explorer

English

The singleton map x ↦ {x} is injective.

Русский

Отображение x ↦ {x} является инъективным.

LaTeX

$$$ \text{Injective}({x} \mapsto \{x\}) $$$

Lean4

theorem singleton_injective : Function.Injective (@singleton ZFSet ZFSet _) := fun x y H =>
  by
  let this := congr_arg sUnion H
  rwa [sUnion_singleton, sUnion_singleton] at this

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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