preperfect_iff_subset_derivedSet

Mathlib.Topology.DerivedSet

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

English

A set U is preperfect if and only if U ⊆ derivedSet U.

Русский

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

LaTeX

$$$$\text{Preperfect}(U) \iff U \subseteq \operatorname{derivedSet}(U).$$$$

Lean4

theorem preperfect_iff_subset_derivedSet {U : Set X} : Preperfect U ↔ U ⊆ derivedSet U :=
  Iff.rfl

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

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

Разделы

Аффилиация

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