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)
172noncomputable def surfaceArea {V : Type*} [Fintype V] [DecidableEq V]
173 (adj : V → V → Prop) [DecidableRel adj]
174 (S : Finset V) : ℕ :=
proof body
Definition body.
175 (S.filter (fun v => ∃ w ∈ Sᶜ, adj v w)).card
176
177/-- Volume of a region: number of vertices. -/
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use