coe_comap

Mathlib.Geometry.Convex.Cone.Pointed

URI: https://scilib.ai/kg/mathlib#PointedCone.coe_comap

English

The carrier of the comap construction coincides with the preimage under the linear map.

Русский

Носитель comap совпадает с предобразом под линейным отображением.

LaTeX

$$ (C.comap f : Set E) = f^{-1}[C] $$

Lean4

@[simp, norm_cast]
theorem coe_comap (f : E →ₗ[R] F) (C : PointedCone R F) : (C.comap f : Set E) = f ⁻¹' C :=
  rfl

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

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

Разделы

Аффилиация

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