Mathlib v3 is deprecated. Go to Mathlib v4

Theorem closure_of_rat_image_lt

Modification history

2018-01-19 17:05

analysis/real.lean

feat(analysis/real): swap out the definition of real, shorten proofs

Added closure_of_rat_image_lt View on Github →