copy — Mathlib

English

Construct an equal copy of a subgraph with possibly different definitional equalities.

Русский

Построить равную копию подграфа с возможной сменой определительных равенств.

LaTeX

$$G'.copy(V'',hV,adj',hadj) = G'$$

Lean4

/-- Create an equal copy of a subgraph (see `copy_eq`) with possibly different definitional equalities.
See Note [range copy pattern].
-/
def copy (G' : Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : V → V → Prop) (hadj : adj' = G'.Adj) : Subgraph G
    where
  verts := V''
  Adj := adj'
  adj_sub := hadj.symm ▸ G'.adj_sub
  edge_vert := hV.symm ▸ hadj.symm ▸ G'.edge_vert
  symm := hadj.symm ▸ G'.symm

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