module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced`

show as: view Lean formalization →

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

generate prose now

used by (1)

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

IndisputableMonolith.Foundation.PublicSpine module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Omniscience module_import

declarations in this module (21)

def DeltaForced L50
def PhysicallyReal L55
theorem physicallyReal_iff_deltaForced L57
def intToNat L71
theorem intToNat_inj L75
def dpair L90
theorem dpair_inj2 L95
theorem rat_eq_of L146
def ratToNat L153
theorem ratToNat_inj L155
theorem deltaForced_nat L162
theorem deltaForced_int L165
theorem deltaForced_rat L169
theorem countable_of_deltaForced L179
theorem not_deltaForced_real L185
theorem forcedTower L200
theorem demarcation L208
theorem deltaForced_iff_countable L222
theorem deltaForced_prod L230
theorem deltaForced_subtype L237
theorem deltaForced_sum L243