def
definition
rs_preserving_RS2VC
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.RSVC on GitHub at line 44.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
41 TrBound : (ℕ → ℕ) → Prop := IsPolynomial
42
43/-- RS‑preserving wrapper bundling sizes and the reduction map. -/
44def rs_preserving_RS2VC : RSPreserving ConstraintInstance VertexCover.Instance :=
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. -/
56def rs_pres_prop : Prop :=
57 Nonempty (Complexity.RSVC.RSPreserving
58 Complexity.RSVC.ConstraintInstance
59 Complexity.VertexCover.Instance)
60
61lemma rs_pres_holds : rs_pres_prop :=
62 ⟨Complexity.RSVC.rs_preserving_RS2VC⟩
63
64end IndisputableMonolith
65
66end IndisputableMonolith