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)
115def LocalResolution {C E : Type*} (r : Recognizer C E) (U : Set C) : Set (Set C) :=
proof body
Definition body.
116 {S : Set C | ∃ c ∈ U, S = U ∩ ResolutionCell r c}
117
118/-- Local resolution cells cover U -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
E
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
ResolutionCell
in IndisputableMonolith.RecogGeom.Indistinguishable
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use