copy — Mathlib

English

Copy of a convex cone with a new carrier equal to the old one.

Русский

Копия выпуклого конуса с новым носителем, равным старому.

LaTeX

$$ConvexCone.copy (C) (s) (hs): ConvexCone R M$$

Lean4

/-- Copy of a convex cone with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[simps]
protected def copy (C : ConvexCone R M) (s : Set M) (hs : s = C) : ConvexCone R M
    where
  carrier := s
  add_mem' := hs.symm ▸ C.add_mem'
  smul_mem' := by simpa [hs] using C.smul_mem'

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