English
The underlying set of the comap of a convex cone by f equals the preimage of the cone under f.
Русский
Подлежащее множество предобраза конуса под f равно предобразу множества конуса под f.
LaTeX
$$ConvexCone.instSetLike.coe (ConvexCone.comap f C) = Set.preimage (LinearMap.instFunLike.coe f) (ConvexCone.instSetLike.coe C)$$
Lean4
/-- The image of a convex cone under a `R`-linear map is a convex cone. -/
def map (f : M →ₗ[R] N) (C : ConvexCone R M) : ConvexCone R N
where
carrier := f '' C
smul_mem' := fun c hc _ ⟨x, hx, hy⟩ => hy ▸ f.map_smul c x ▸ mem_image_of_mem f (C.smul_mem hc hx)
add_mem' := fun _ ⟨x₁, hx₁, hy₁⟩ _ ⟨x₂, hx₂, hy₂⟩ =>
hy₁ ▸ hy₂ ▸ f.map_add x₁ x₂ ▸ mem_image_of_mem f (add_mem hx₁ hx₂)
