pith. machine review for the scientific record. sign in
def definition def or abbrev

rs_preserving_RS2VC

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  44def rs_preserving_RS2VC : RSPreserving ConstraintInstance VertexCover.Instance :=

proof body

Definition body.

  45{ sizeA := fun a => a.vertices.length + a.constraints.length
  46, sizeB := fun b => b.vertices.length + b.edges.length
  47, reduce := reduceRS2VC }
  48
  49end RSVC
  50
  51end Complexity
  52
  53namespace IndisputableMonolith
  54
  55/-- RS‑preserving reduction existence as a Prop. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.