IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal

declarations in this module (40)

• structure RatInterval L43
• def width L51
• theorem width_nonneg L53
• def Subset L57
• def Overlap L60
• structure Protocol L69
• def lo L77
• def hi L80
• theorem lo_le_hi L82
• theorem lo_mono L85
• theorem hi_anti L91
• theorem lo_le_hi_cross L98
• theorem bddAbove_lo L104
• def value L111
• theorem lo_le_value L113
• theorem value_le_hi L116
• theorem value_mem L120
• theorem width_real_bound L123
• theorem tiny_le_zero L136
• theorem value_unique L149
• def ObsEq L165
• theorem obsEq_iff_value L170
• theorem obsEq_refl L211
• theorem obsEq_symm L213
• theorem obsEq_trans L216
• def obsSetoid L220
• def ofRat L227
• theorem value_ofRat L235
• theorem ofRat_obsEq_iff L241
• def add L249
• theorem value_add L299
• def neg L322
• theorem value_neg L334
• def sub L353
• theorem value_sub L355
• theorem floor_double L364
• def canonical L381
• theorem value_canonical L432
• theorem value_surjective L452
• theorem display_real_forgetful L470