image_coev

Mathlib.Topology.CompactOpen

URI: https://scilib.ai/kg/mathlib#ContinuousMap.image_coev

English

The image of a subset s under the coevaluation map is exactly {y} × s for a fixed y ∈ Y.

Русский

Образ множества s при ковеировании равен {y} × s для фиксированного y ∈ Y.

LaTeX

$$$\text{image}(\operatorname{coev} y\, ''\, s) = \{y\} \times s$$$

Lean4

theorem image_coev {y : Y} (s : Set X) : coev X Y y '' s = { y } ×ˢ s := by simp [singleton_prod]

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

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

Разделы

Аффилиация

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