perfect_iff_eq_derivedSet

Mathlib.Topology.DerivedSet

URI: https://scilib.ai/kg/mathlib#perfect_iff_eq_derivedSet

← MathLib Explorer

English

A set U is perfect if and only if U = derivedSet(U).

Русский

Множество U идеальное тогда и только тогда, когда U равно derivedSet(U).

LaTeX

$$$$\text{Perfect}(U) \iff U = \operatorname{derivedSet}(U).$$$$

Lean4

theorem perfect_iff_eq_derivedSet {U : Set X} : Perfect U ↔ U = derivedSet U := by
  rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet, ← subset_antisymm_iff, eq_comm]

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

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

Разделы

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

Аффилиация

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