lemma
proved
term proof
Z_of_window_zero
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)
26@[simp] lemma Z_of_window_zero (w : Pattern 0) : Z_of_window w = 0 := by
proof body
Term-mode proof.
27 simp [Z_of_window]
28
29/-- The cylinder set of streams whose first `n` bits coincide with the window `w`. -/
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
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
-
Pattern
in IndisputableMonolith.Measurement
decl_use
-
Z_of_window
in IndisputableMonolith.Measurement
decl_use
-
Pattern
in IndisputableMonolith.Patterns
decl_use
-
Pattern
in IndisputableMonolith.Streams
decl_use
-
Z_of_window
in IndisputableMonolith.Streams
decl_use
-
Pattern
in IndisputableMonolith.Streams.Blocks
decl_use
-
Z_of_window
in IndisputableMonolith.Streams.Blocks
decl_use