eq_deltaGenerated

Mathlib.Topology.Compactness.DeltaGeneratedSpace

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

English

For any X, if DeltaGeneratedSpace X holds, then tX equals deltaGenerated X.

Русский

Для любого X, если DeltaGeneratedSpace X выполняется, тогда tX = deltaGenerated X.

LaTeX

$$$[\\DeltaGeneratedSpace X] \\Rightarrow t_X = \\deltaGenerated(X)$$$

Lean4

theorem eq_deltaGenerated [DeltaGeneratedSpace X] : tX = deltaGenerated X :=
  eq_of_le_of_ge DeltaGeneratedSpace.le_deltaGenerated deltaGenerated_le

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

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

Разделы

Аффилиация

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