module
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FiniteCertificateTransfer
show as:
view Lean formalization →
used by (3)
depends on (1)
declarations in this module (14)
-
structure
TypedFiniteDistinction -
structure
CertificateMap -
def
LegitimateContinuumStatement -
theorem
certificateMap_legitimate -
theorem
conservative_completion_transfers -
theorem
obstruction_descends -
theorem
finite_certificate_transfer -
structure
SoundFaithfulCover -
theorem
everything_certified_not_faithful -
theorem
soundFaithfulCover_injects -
theorem
soundFaithfulCover_countable_witnesses -
theorem
no_soundFaithfulCover_of_uncountable_witnesses -
theorem
reals_uncountable_witnesses -
theorem
no_sound_faithful_certification_of_reals