copy — Mathlib

English

Copy a substructure by replacing its carrier with a set equal to it, preserving the operation interpretation.

Русский

Скопируйте подструктуру, замещая её носитель на множество, равное ему, сохраняющи отображение операций.

LaTeX

$$$$ S.copy\; s\; hs = S $$$$

Lean4

/-- Copy a substructure replacing `carrier` with a set that is equal to it. -/
protected def copy (S : L.Substructure M) (s : Set M) (hs : s = S) : L.Substructure M
    where
  carrier := s
  fun_mem _ f := hs.symm ▸ S.fun_mem _ f

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