structure definition def or abbrev

`Instance`

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

formal statement (Lean)

  14structure Instance where
  15  vertices : List Nat
  16  edges    : List (Nat × Nat)
  17  k        : Nat
  18  deriving Repr
  19
  20/-- A set `S` covers an edge `(u,v)` if it contains `u` or `v`. -/

used by (13)

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

reduceRS2VC in IndisputableMonolith.Complexity.RSVC decl_use
rs_preserving_RS2VC in IndisputableMonolith.Complexity.RSVC decl_use
rs_pres_prop in IndisputableMonolith.Complexity.RSVC decl_use
toVC in IndisputableMonolith.Complexity.RSVC decl_use
Covers in IndisputableMonolith.Complexity.VertexCover decl_use
Covers_nil_edges in IndisputableMonolith.Complexity.VertexCover decl_use
HasCover in IndisputableMonolith.Complexity.VertexCover decl_use
hasCover_of_nil_edges in IndisputableMonolith.Complexity.VertexCover decl_use
trivialInstance in IndisputableMonolith.Complexity.VertexCover decl_use
dAlembert_contDiff_top in IndisputableMonolith.Cost.AczelProof decl_use
universal_cost_certificate in IndisputableMonolith.NumberTheory.UniversalCostSpectrum decl_use
countLaw_implies_no_extra in IndisputableMonolith.Patterns.TwoToTheDMinusOne decl_use
coneEntropyStub in IndisputableMonolith.Relativity.NewFixtures decl_use

depends on (7)

Lean names referenced from this declaration's body.

or in IndisputableMonolith.Constants.EulerMascheroni decl_use
contains in IndisputableMonolith.Ethics.StakeGraph decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
contains in IndisputableMonolith.Numerics.Interval.Basic decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use