theorem proved term proof

`primeSupport_directed`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  42theorem primeSupport_directed (S T : PrimeSupport) :
  43    ∃ U : PrimeSupport, S ⊆ U ∧ T ⊆ U := by

Term-mode proof.

  44  exact ⟨S ∪ T, Finset.subset_union_left, Finset.subset_union_right⟩
  45
  46/-- Prime-event membership persists under support enlargement. -/

From the project-wide theorem graph. These declarations reference this one in their body.

concreteDirectedEulerLedgerSystem in IndisputableMonolith.NumberTheory.DirectedEulerLedger decl_use

Lean names referenced from this declaration's body.

U in IndisputableMonolith.Constants.RSNativeUnits decl_use
T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
PrimeSupport in IndisputableMonolith.NumberTheory.DirectedEulerLedger decl_use
Prime in IndisputableMonolith.NumberTheory.Primes.Basic decl_use
U in IndisputableMonolith.Recognition decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use