def
definition
rs_pres_prop
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Complexity.RSVC on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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