Commit 2024-07-04 11:38 e8574fb4

View on Github →

feat(Topology/Instances/EReal): lemmas related to liminf and limsup (#14128) Changes:

  • Add liminf_le_liminf
  • Add limsup_le_limsup
  • Add limsup_add_le_lt₂
  • Add limsup_add_bot_ne_top
  • Add limsup_add_le_add_limsup
  • Add ge_iff_le_forall_real_lt
  • Add liminf_add_ge_gt₂
  • Add liminf_add_top_ne_bot
  • Add add_liminf_le_liminf_add
  • Add limsup_le_iff
  • Add limsup_le_const_forall
  • Add const_le_limsup_forall
  • Add liminf_le_const_forall
  • Add const_le_liminf_forall
  • Add limsup_max

Estimated changes

added theorem EReal.max_neg_neg
added theorem EReal.min_neg_neg
added theorem EReal.neg_add
added theorem EReal.neg_sub
added theorem EReal.liminf_le_liminf
added theorem EReal.liminf_neg
added theorem EReal.limsup_le_iff
added theorem EReal.limsup_le_limsup
added theorem EReal.limsup_neg