comap — Mathlib

English

The comap by the identity map is the cone itself.

Русский

Предобраз конуса по тождественному отображению совпадает с конусом.

LaTeX

$$C.comap LinearMap.id = C$$

Lean4

/-- The preimage of a convex cone under a `R`-linear map is a convex cone. -/
def comap (f : M →ₗ[R] N) (C : ConvexCone R N) : ConvexCone R M
    where
  carrier := f ⁻¹' C
  smul_mem' c hc x
    hx := by
    rw [mem_preimage, f.map_smul c]
    exact C.smul_mem hc hx
  add_mem' x hx y
    hy := by
    rw [mem_preimage, f.map_add]
    exact add_mem hx hy

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