module module

`IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LogicAsFunctionalEquation.MainTheorem module_import

declarations in this module (7)

structure FiniteBooleanReality L17
def eventWeight L24
def EventNonempty L29
theorem eventWeight_pos L33
def eventRatio L52
theorem eventRatio_pos L57
theorem finite_boolean_logic_embeds_into_positive_ratios L66