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)
494theorem RSReal_synth_iff {U : Type*} {D : Set U} {F : U → ℝ} {x : ℝ} :
495 RSReal_synth D F x ↔ x = 1 ∧ ∃ u ∈ D, x = F u := by
proof body
Term-mode proof.
496 simp only [RSReal_synth, rs_exists_unique_one]
497
498/-- The φ-ladder as a specific discrete skeleton. -/
depends on (8)
Lean names referenced from this declaration's body.
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
rs_exists_unique_one
in IndisputableMonolith.Foundation.OntologyPredicates
decl_use
-
RSReal_synth
in IndisputableMonolith.Foundation.OntologyPredicates
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use