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)
35instance finConfigSpace (n : ℕ) [h : NeZero n] : ConfigSpace (Fin n) where
36 nonempty := ⟨0⟩
proof body
Definition body.
37
38/-- The discrete recognizer: identity map (distinguishes everything) -/
depends on (6)
Lean names referenced from this declaration's body.
-
ConfigSpace
in IndisputableMonolith.Foundation.CostFromDistinction
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
ConfigSpace
in IndisputableMonolith.Modal.Possibility
decl_use
-
ConfigSpace
in IndisputableMonolith.RecogGeom.Core
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use