continuous_counit

Mathlib.Topology.Compactness.DeltaGeneratedSpace

URI: https://scilib.ai/kg/mathlib#DeltaGeneratedSpace.continuous_counit

English

The counit map from the delta-generated space on X to X is continuous.

Русский

Пусть counit: ΔGeneratedSpace on X → X, тогда он непрерывен.

LaTeX

$$$$\text{Continuous}(\mathrm{counit} : \DeltaGeneratedSpace X \to X).$$$$

Lean4

theorem continuous_counit : Continuous (counit : _ → X) := by rw [continuous_iff_coinduced_le]; exact deltaGenerated_le

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

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

Разделы

Аффилиация

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