Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-07 19:03 820bac36

View on Github →

building the hyperreal library (#835)

  • more instances
  • fix stuff that got weirded
  • fix stuff that got weird
  • fix stuff that became weird
  • build hyperreal library (with sorries)
  • fix weirdness, prettify etc.
  • spaces
  • st lt le lemmas fix type
  • Update src/data/real/hyperreal.lean Co-Authored-By: abhimanyupallavisudhir 43954672+abhimanyupallavisudhir@users.noreply.github.com
  • if then
  • more stuff
  • Update hyperreal.lean
  • Update hyperreal.lean
  • Update basic.lean
  • Update basic.lean
  • Update hyperreal.lean
  • of_max, of_min, of_abs
  • Update filter_product.lean
  • Update hyperreal.lean
  • abs_def etc.
  • Update filter_product.lean
  • hole
  • Update hyperreal.lean
  • Update filter_product.lean
  • Update filter_product.lean
  • Update filter_product.lean
  • Update hyperreal.lean
  • Update hyperreal.lean
  • Update filter_product.lean
  • Update hyperreal.lean
  • Update hyperreal.lean
  • finally done with all sorries!
  • Update hyperreal.lean
  • fix (?)
  • fix (?) ring issue
  • real.Sup_univ
  • st is Sup
  • st_id_real spacebar
  • sup --> Sup
  • fix weirds
  • dollar signs
  • 100-column
  • 100 columns rule
  • Update hyperreal.lean
  • removing uparrows
  • uparrows
  • some stuff that got away
  • fix
  • lift_id
  • fix?
  • fix mono, hopefully
  • fix mono, hopefully
  • this should work
  • fix -- no more mono
  • fixes
  • fixes
  • fixes
  • fixes
  • ok, fixed

Estimated changes

modified theorem hyperreal.epsilon_lt_pos
added theorem hyperreal.is_st_Sup
added theorem hyperreal.is_st_add
added theorem hyperreal.is_st_inv
added theorem hyperreal.is_st_mul
added theorem hyperreal.is_st_neg
added theorem hyperreal.is_st_st'
added theorem hyperreal.is_st_st
added theorem hyperreal.is_st_sub
modified theorem hyperreal.is_st_unique
added theorem hyperreal.lt_of_st_lt
added theorem hyperreal.st_add
added theorem hyperreal.st_eq_Sup
added theorem hyperreal.st_id_real
added theorem hyperreal.st_infinite
added theorem hyperreal.st_inv
added theorem hyperreal.st_le_of_le
added theorem hyperreal.st_mul
added theorem hyperreal.st_neg
added theorem hyperreal.st_of_is_st