Commit 2023-06-16 17:54 20944407

View on Github →

feat: port Counterexamples.MapFloor (#5147)

Estimated changes

Modified Counterexamples.lean

Created Counterexamples/MapFloor.lean

added def Counterexample.IntWithEpsilon.forgetEpsilons

added theorem Counterexample.IntWithEpsilon.forgetEpsilons_apply

added theorem Counterexample.IntWithEpsilon.forgetEpsilons_floor_lt

added theorem Counterexample.IntWithEpsilon.lt_forgetEpsilons_ceil

added theorem Counterexample.IntWithEpsilon.pos_iff

added def Counterexample.IntWithEpsilon