coe_comap

Mathlib.Analysis.Convex.Cone.Basic

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

English

The underlying set of C.comap f equals the preimage f^{-1}(C).

Русский

Множество C.comap f равно предобразованию f^{-1}(C).

LaTeX

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

Lean4

@[simp]
theorem coe_comap (f : E →L[R] F) (C : ProperCone R F) : (C.comap f : Set E) = f ⁻¹' C :=
  rfl

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

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

Разделы

Аффилиация

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