module module

`IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction`

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.DistinctionToT4 module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.BooleanProjectionFromMark module_import
IndisputableMonolith.Foundation.ObservableFloorWitness module_import

declarations in this module (19)

def markedPairOfDistinction L43
def forcedBoolProjection L50
theorem forcedBoolProjection_base L54
theorem forcedBoolProjection_alt L59
def forcedObservableSetoid L69
theorem forcedObservableFloor L83
theorem forcedQuotientNontrivial L91
def forcedQuotientToBool L100
def forcedBoolRepresentative L108
theorem forcedQuotientToBool_representative L116
theorem forcedBoolRepresentative_left_inv L122
def forcedQuotientEquivBool L145
structure ForcedBooleanCoordinates L156
def canonicalForcedBooleanCoordinates L160
def forcedBooleanCoordinateChange L167
theorem forcedBooleanCoordinates_unique_up_to_bool_aut L174
theorem rawFloor_forced_from_distinction L191
theorem booleanObservableFloor_forced_from_distinction L197
theorem bool_distinction L203