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)
23def EdgeCovered (S : List Nat) (e : Nat × Nat) : Prop :=
proof body
Definition body.
24 InCover S e.fst ∨ InCover S e.snd
25
26/-- `S` covers all edges of instance `I`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
Covers
in IndisputableMonolith.Complexity.VertexCover
decl_use
-
EdgeCovered_comm
in IndisputableMonolith.Complexity.VertexCover
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
InCover
in IndisputableMonolith.Complexity.VertexCover
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use