Documentation

Mathlib.Data.Real.Hyperreal

Construction of the hyperreal numbers as an ultraproduct of real sequences. #

Hyperreal numbers on the ultrafilter extending the cofinite filter

Equations
Instances For

    Hyperreal numbers on the ultrafilter extending the cofinite filter

    Equations
    Instances For

      Natural embedding ℝ → ℝ*.

      Equations
      Instances For
        @[simp]
        theorem Hyperreal.coe_eq_coe {x : } {y : } :
        x = y x = y
        theorem Hyperreal.coe_ne_coe {x : } {y : } :
        x y x y
        @[simp]
        theorem Hyperreal.coe_eq_zero {x : } :
        x = 0 x = 0
        @[simp]
        theorem Hyperreal.coe_eq_one {x : } :
        x = 1 x = 1
        theorem Hyperreal.coe_ne_zero {x : } :
        x 0 x 0
        theorem Hyperreal.coe_ne_one {x : } :
        x 1 x 1
        @[simp]
        theorem Hyperreal.coe_one :
        1 = 1
        @[simp]
        theorem Hyperreal.coe_zero :
        0 = 0
        @[simp]
        theorem Hyperreal.coe_inv (x : ) :
        x⁻¹ = (↑x)⁻¹
        @[simp]
        theorem Hyperreal.coe_neg (x : ) :
        (-x) = -x
        @[simp]
        theorem Hyperreal.coe_add (x : ) (y : ) :
        (x + y) = x + y
        @[simp]
        theorem Hyperreal.coe_ofNat (n : ) [n.AtLeastTwo] :
        @[simp]
        theorem Hyperreal.coe_mul (x : ) (y : ) :
        (x * y) = x * y
        @[simp]
        theorem Hyperreal.coe_div (x : ) (y : ) :
        (x / y) = x / y
        @[simp]
        theorem Hyperreal.coe_sub (x : ) (y : ) :
        (x - y) = x - y
        @[simp]
        theorem Hyperreal.coe_le_coe {x : } {y : } :
        x y x y
        @[simp]
        theorem Hyperreal.coe_lt_coe {x : } {y : } :
        x < y x < y
        @[simp]
        theorem Hyperreal.coe_nonneg {x : } :
        0 x 0 x
        @[simp]
        theorem Hyperreal.coe_pos {x : } :
        0 < x 0 < x
        @[simp]
        theorem Hyperreal.coe_abs (x : ) :
        |x| = |x|
        @[simp]
        theorem Hyperreal.coe_max (x : ) (y : ) :
        (max x y) = max x y
        @[simp]
        theorem Hyperreal.coe_min (x : ) (y : ) :
        (min x y) = min x y
        def Hyperreal.ofSeq (f : ) :

        Construct a hyperreal number from a sequence of real numbers.

        Equations
        Instances For
          theorem Hyperreal.ofSeq_lt_ofSeq {f : } {g : } :
          Hyperreal.ofSeq f < Hyperreal.ofSeq g ∀ᶠ (n : ) in (Filter.hyperfilter ), f n < g n
          noncomputable def Hyperreal.epsilon :

          A sample infinitesimal hyperreal

          Equations
          Instances For
            noncomputable def Hyperreal.omega :

            A sample infinite hyperreal

            Equations
            Instances For

              A sample infinitesimal hyperreal

              Equations
              Instances For

                A sample infinite hyperreal

                Equations
                Instances For
                  theorem Hyperreal.lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
                  0 < rHyperreal.ofSeq f < r
                  theorem Hyperreal.neg_lt_of_tendsto_zero_of_pos {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
                  0 < r-r < Hyperreal.ofSeq f
                  theorem Hyperreal.gt_of_tendsto_zero_of_neg {f : } (hf : Filter.Tendsto f Filter.atTop (nhds 0)) {r : } :
                  r < 0r < Hyperreal.ofSeq f
                  def Hyperreal.IsSt (x : ℝ*) (r : ) :

                  Standard part predicate

                  Equations
                  • x.IsSt r = ∀ (δ : ), 0 < δr - δ < x x < r + δ
                  Instances For
                    noncomputable def Hyperreal.st :
                    ℝ*

                    Standard part function: like a "round" to ℝ instead of ℤ

                    Equations
                    Instances For

                      A hyperreal number is infinitesimal if its standard part is 0

                      Equations
                      • x.Infinitesimal = x.IsSt 0
                      Instances For

                        A hyperreal number is positive infinite if it is larger than all real numbers

                        Equations
                        • x.InfinitePos = ∀ (r : ), r < x
                        Instances For

                          A hyperreal number is negative infinite if it is smaller than all real numbers

                          Equations
                          • x.InfiniteNeg = ∀ (r : ), x < r
                          Instances For

                            A hyperreal number is infinite if it is infinite positive or infinite negative

                            Equations
                            • x.Infinite = (x.InfinitePos x.InfiniteNeg)
                            Instances For

                              Some facts about st #

                              theorem Hyperreal.isSt_of_tendsto {f : } {r : } (hf : Filter.Tendsto f Filter.atTop (nhds r)) :
                              (Hyperreal.ofSeq f).IsSt r
                              theorem Hyperreal.IsSt.lt {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) (hrs : r < s) :
                              x < y
                              theorem Hyperreal.IsSt.unique {x : ℝ*} {r : } {s : } (hr : x.IsSt r) (hs : x.IsSt s) :
                              r = s
                              theorem Hyperreal.IsSt.st_eq {x : ℝ*} {r : } (hxr : x.IsSt r) :
                              x.st = r
                              theorem Hyperreal.IsSt.not_infinite {x : ℝ*} {r : } (h : x.IsSt r) :
                              ¬x.Infinite
                              theorem Hyperreal.not_infinite_of_exists_st {x : ℝ*} :
                              (∃ (r : ), x.IsSt r)¬x.Infinite
                              theorem Hyperreal.Infinite.st_eq {x : ℝ*} (hi : x.Infinite) :
                              x.st = 0
                              theorem Hyperreal.isSt_sSup {x : ℝ*} (hni : ¬x.Infinite) :
                              x.IsSt (sSup {y : | y < x})
                              theorem Hyperreal.exists_st_of_not_infinite {x : ℝ*} (hni : ¬x.Infinite) :
                              ∃ (r : ), x.IsSt r
                              theorem Hyperreal.st_eq_sSup {x : ℝ*} :
                              x.st = sSup {y : | y < x}
                              theorem Hyperreal.exists_st_iff_not_infinite {x : ℝ*} :
                              (∃ (r : ), x.IsSt r) ¬x.Infinite
                              theorem Hyperreal.infinite_iff_not_exists_st {x : ℝ*} :
                              x.Infinite ¬∃ (r : ), x.IsSt r
                              theorem Hyperreal.IsSt.isSt_st {x : ℝ*} {r : } (hxr : x.IsSt r) :
                              x.IsSt x.st
                              theorem Hyperreal.isSt_st_of_exists_st {x : ℝ*} (hx : ∃ (r : ), x.IsSt r) :
                              x.IsSt x.st
                              theorem Hyperreal.isSt_st' {x : ℝ*} (hx : ¬x.Infinite) :
                              x.IsSt x.st
                              theorem Hyperreal.isSt_st {x : ℝ*} (hx : x.st 0) :
                              x.IsSt x.st
                              theorem Hyperreal.isSt_refl_real (r : ) :
                              (↑r).IsSt r
                              theorem Hyperreal.st_id_real (r : ) :
                              (↑r).st = r
                              theorem Hyperreal.eq_of_isSt_real {r : } {s : } :
                              (↑r).IsSt sr = s
                              theorem Hyperreal.isSt_real_iff_eq {r : } {s : } :
                              (↑r).IsSt s r = s
                              theorem Hyperreal.isSt_symm_real {r : } {s : } :
                              (↑r).IsSt s (↑s).IsSt r
                              theorem Hyperreal.isSt_trans_real {r : } {s : } {t : } :
                              (↑r).IsSt s(↑s).IsSt t(↑r).IsSt t
                              theorem Hyperreal.isSt_inj_real {r₁ : } {r₂ : } {s : } (h1 : (↑r₁).IsSt s) (h2 : (↑r₂).IsSt s) :
                              r₁ = r₂
                              theorem Hyperreal.isSt_iff_abs_sub_lt_delta {x : ℝ*} {r : } :
                              x.IsSt r ∀ (δ : ), 0 < δ|x - r| < δ
                              theorem Hyperreal.IsSt.map {x : ℝ*} {r : } (hxr : x.IsSt r) {f : } (hf : ContinuousAt f r) :
                              theorem Hyperreal.IsSt.map₂ {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) {f : } (hf : ContinuousAt (Function.uncurry f) (r, s)) :
                              theorem Hyperreal.IsSt.add {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
                              (x + y).IsSt (r + s)
                              theorem Hyperreal.IsSt.neg {x : ℝ*} {r : } (hxr : x.IsSt r) :
                              (-x).IsSt (-r)
                              theorem Hyperreal.IsSt.sub {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
                              (x - y).IsSt (r - s)
                              theorem Hyperreal.IsSt.le {x : ℝ*} {y : ℝ*} {r : } {s : } (hrx : x.IsSt r) (hsy : y.IsSt s) (hxy : x y) :
                              r s
                              theorem Hyperreal.st_le_of_le {x : ℝ*} {y : ℝ*} (hix : ¬x.Infinite) (hiy : ¬y.Infinite) :
                              x yx.st y.st
                              theorem Hyperreal.lt_of_st_lt {x : ℝ*} {y : ℝ*} (hix : ¬x.Infinite) (hiy : ¬y.Infinite) :
                              x.st < y.stx < y

                              Basic lemmas about infinite #

                              theorem Hyperreal.infinitePos_def {x : ℝ*} :
                              x.InfinitePos ∀ (r : ), r < x
                              theorem Hyperreal.infiniteNeg_def {x : ℝ*} :
                              x.InfiniteNeg ∀ (r : ), x < r
                              theorem Hyperreal.InfinitePos.pos {x : ℝ*} (hip : x.InfinitePos) :
                              0 < x
                              theorem Hyperreal.InfiniteNeg.lt_zero {x : ℝ*} :
                              x.InfiniteNegx < 0
                              theorem Hyperreal.Infinite.ne_zero {x : ℝ*} (hI : x.Infinite) :
                              x 0
                              theorem Hyperreal.InfiniteNeg.not_infinitePos {x : ℝ*} :
                              x.InfiniteNeg¬x.InfinitePos
                              theorem Hyperreal.InfinitePos.not_infiniteNeg {x : ℝ*} (hp : x.InfinitePos) :
                              ¬x.InfiniteNeg
                              theorem Hyperreal.InfinitePos.neg {x : ℝ*} :
                              x.InfinitePos(-x).InfiniteNeg
                              theorem Hyperreal.InfiniteNeg.neg {x : ℝ*} :
                              x.InfiniteNeg(-x).InfinitePos
                              @[simp]
                              theorem Hyperreal.infiniteNeg_neg {x : ℝ*} :
                              (-x).InfiniteNeg x.InfinitePos
                              @[simp]
                              theorem Hyperreal.infinitePos_neg {x : ℝ*} :
                              (-x).InfinitePos x.InfiniteNeg
                              @[simp]
                              theorem Hyperreal.infinite_neg {x : ℝ*} :
                              (-x).Infinite x.Infinite
                              theorem Hyperreal.Infinitesimal.not_infinite {x : ℝ*} (h : x.Infinitesimal) :
                              ¬x.Infinite
                              theorem Hyperreal.Infinite.not_infinitesimal {x : ℝ*} (h : x.Infinite) :
                              ¬x.Infinitesimal
                              theorem Hyperreal.InfinitePos.not_infinitesimal {x : ℝ*} (h : x.InfinitePos) :
                              ¬x.Infinitesimal
                              theorem Hyperreal.InfiniteNeg.not_infinitesimal {x : ℝ*} (h : x.InfiniteNeg) :
                              ¬x.Infinitesimal
                              theorem Hyperreal.infinitePos_iff_infinite_and_pos {x : ℝ*} :
                              x.InfinitePos x.Infinite 0 < x
                              theorem Hyperreal.infiniteNeg_iff_infinite_and_neg {x : ℝ*} :
                              x.InfiniteNeg x.Infinite x < 0
                              theorem Hyperreal.infinitePos_iff_infinite_of_nonneg {x : ℝ*} (hp : 0 x) :
                              x.InfinitePos x.Infinite
                              theorem Hyperreal.infinitePos_iff_infinite_of_pos {x : ℝ*} (hp : 0 < x) :
                              x.InfinitePos x.Infinite
                              theorem Hyperreal.infiniteNeg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) :
                              x.InfiniteNeg x.Infinite
                              theorem Hyperreal.infinitePos_abs_iff_infinite_abs {x : ℝ*} :
                              |x|.InfinitePos |x|.Infinite
                              @[simp]
                              theorem Hyperreal.infinite_abs_iff {x : ℝ*} :
                              |x|.Infinite x.Infinite
                              @[simp]
                              theorem Hyperreal.infinitePos_abs_iff_infinite {x : ℝ*} :
                              |x|.InfinitePos x.Infinite
                              theorem Hyperreal.infinite_iff_abs_lt_abs {x : ℝ*} :
                              x.Infinite ∀ (r : ), |r| < |x|
                              theorem Hyperreal.infinitePos_add_not_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              x.InfinitePos¬y.InfiniteNeg(x + y).InfinitePos
                              theorem Hyperreal.not_infiniteNeg_add_infinitePos {x : ℝ*} {y : ℝ*} :
                              ¬x.InfiniteNegy.InfinitePos(x + y).InfinitePos
                              theorem Hyperreal.infiniteNeg_add_not_infinitePos {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNeg¬y.InfinitePos(x + y).InfiniteNeg
                              theorem Hyperreal.not_infinitePos_add_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              ¬x.InfinitePosy.InfiniteNeg(x + y).InfiniteNeg
                              theorem Hyperreal.infinitePos_add_infinitePos {x : ℝ*} {y : ℝ*} :
                              x.InfinitePosy.InfinitePos(x + y).InfinitePos
                              theorem Hyperreal.infiniteNeg_add_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNegy.InfiniteNeg(x + y).InfiniteNeg
                              theorem Hyperreal.infinitePos_add_not_infinite {x : ℝ*} {y : ℝ*} :
                              x.InfinitePos¬y.Infinite(x + y).InfinitePos
                              theorem Hyperreal.infiniteNeg_add_not_infinite {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNeg¬y.Infinite(x + y).InfiniteNeg
                              theorem Hyperreal.infinitePos_of_tendsto_top {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atTop) :
                              (Hyperreal.ofSeq f).InfinitePos
                              theorem Hyperreal.infiniteNeg_of_tendsto_bot {f : } (hf : Filter.Tendsto f Filter.atTop Filter.atBot) :
                              (Hyperreal.ofSeq f).InfiniteNeg
                              theorem Hyperreal.not_infinite_neg {x : ℝ*} :
                              ¬x.Infinite¬(-x).Infinite
                              theorem Hyperreal.not_infinite_add {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) :
                              ¬(x + y).Infinite
                              theorem Hyperreal.not_infinite_iff_exist_lt_gt {x : ℝ*} :
                              ¬x.Infinite ∃ (r : ) (s : ), r < x x < s
                              theorem Hyperreal.not_infinite_real (r : ) :
                              ¬(↑r).Infinite
                              theorem Hyperreal.Infinite.ne_real {x : ℝ*} :
                              x.Infinite∀ (r : ), x r

                              Facts about st that require some infinite machinery #

                              theorem Hyperreal.IsSt.mul {x : ℝ*} {y : ℝ*} {r : } {s : } (hxr : x.IsSt r) (hys : y.IsSt s) :
                              (x * y).IsSt (r * s)
                              theorem Hyperreal.not_infinite_mul {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) :
                              ¬(x * y).Infinite
                              theorem Hyperreal.st_add {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) :
                              (x + y).st = x.st + y.st
                              theorem Hyperreal.st_neg (x : ℝ*) :
                              (-x).st = -x.st
                              theorem Hyperreal.st_mul {x : ℝ*} {y : ℝ*} (hx : ¬x.Infinite) (hy : ¬y.Infinite) :
                              (x * y).st = x.st * y.st

                              Basic lemmas about infinitesimal #

                              theorem Hyperreal.infinitesimal_def {x : ℝ*} :
                              x.Infinitesimal ∀ (r : ), 0 < r-r < x x < r
                              theorem Hyperreal.lt_of_pos_of_infinitesimal {x : ℝ*} :
                              x.Infinitesimal∀ (r : ), 0 < rx < r
                              theorem Hyperreal.lt_neg_of_pos_of_infinitesimal {x : ℝ*} :
                              x.Infinitesimal∀ (r : ), 0 < r-r < x
                              theorem Hyperreal.gt_of_neg_of_infinitesimal {x : ℝ*} (hi : x.Infinitesimal) (r : ) (hr : r < 0) :
                              r < x
                              theorem Hyperreal.abs_lt_real_iff_infinitesimal {x : ℝ*} :
                              x.Infinitesimal ∀ (r : ), r 0|x| < |r|
                              theorem Hyperreal.Infinitesimal.eq_zero {r : } :
                              (↑r).Infinitesimalr = 0
                              @[simp]
                              theorem Hyperreal.infinitesimal_real_iff {r : } :
                              (↑r).Infinitesimal r = 0
                              theorem Hyperreal.Infinitesimal.add {x : ℝ*} {y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) :
                              (x + y).Infinitesimal
                              theorem Hyperreal.Infinitesimal.neg {x : ℝ*} (hx : x.Infinitesimal) :
                              (-x).Infinitesimal
                              @[simp]
                              theorem Hyperreal.infinitesimal_neg {x : ℝ*} :
                              (-x).Infinitesimal x.Infinitesimal
                              theorem Hyperreal.Infinitesimal.mul {x : ℝ*} {y : ℝ*} (hx : x.Infinitesimal) (hy : y.Infinitesimal) :
                              (x * y).Infinitesimal
                              theorem Hyperreal.infinitesimal_of_tendsto_zero {f : } (h : Filter.Tendsto f Filter.atTop (nhds 0)) :
                              (Hyperreal.ofSeq f).Infinitesimal
                              theorem Hyperreal.not_real_of_infinitesimal_ne_zero (x : ℝ*) :
                              x.Infinitesimalx 0∀ (r : ), x r
                              theorem Hyperreal.IsSt.infinitesimal_sub {x : ℝ*} {r : } (hxr : x.IsSt r) :
                              (x - r).Infinitesimal
                              theorem Hyperreal.infinitesimal_sub_st {x : ℝ*} (hx : ¬x.Infinite) :
                              (x - x.st).Infinitesimal
                              theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos {x : ℝ*} :
                              x.InfinitePos x⁻¹.Infinitesimal 0 < x⁻¹
                              theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg {x : ℝ*} :
                              x.InfiniteNeg x⁻¹.Infinitesimal x⁻¹ < 0
                              theorem Hyperreal.infinitesimal_inv_of_infinite {x : ℝ*} :
                              x.Infinitex⁻¹.Infinitesimal
                              theorem Hyperreal.infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x 0) (hi : x⁻¹.Infinitesimal) :
                              x.Infinite
                              theorem Hyperreal.infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x 0) :
                              x.Infinite x⁻¹.Infinitesimal
                              theorem Hyperreal.infinitesimal_pos_iff_infinitePos_inv {x : ℝ*} :
                              x⁻¹.InfinitePos x.Infinitesimal 0 < x
                              theorem Hyperreal.infinitesimal_neg_iff_infiniteNeg_inv {x : ℝ*} :
                              x⁻¹.InfiniteNeg x.Infinitesimal x < 0
                              theorem Hyperreal.infinitesimal_iff_infinite_inv {x : ℝ*} (h : x 0) :
                              x.Infinitesimal x⁻¹.Infinite

                              Hyperreal.st stuff that requires infinitesimal machinery #

                              theorem Hyperreal.IsSt.inv {x : ℝ*} {r : } (hi : ¬x.Infinitesimal) (hr : x.IsSt r) :
                              x⁻¹.IsSt r⁻¹
                              theorem Hyperreal.st_inv (x : ℝ*) :
                              x⁻¹.st = x.st⁻¹

                              Infinite stuff that requires infinitesimal machinery #

                              theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} :
                              x.InfinitePos¬y.Infinitesimal0 < y(x * y).InfinitePos
                              theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_pos_infinitePos {x : ℝ*} {y : ℝ*} :
                              ¬x.Infinitesimal0 < xy.InfinitePos(x * y).InfinitePos
                              theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNeg¬y.Infinitesimaly < 0(x * y).InfinitePos
                              theorem Hyperreal.infinitePos_mul_of_not_infinitesimal_neg_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              ¬x.Infinitesimalx < 0y.InfiniteNeg(x * y).InfinitePos
                              theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg {x : ℝ*} {y : ℝ*} :
                              x.InfinitePos¬y.Infinitesimaly < 0(x * y).InfiniteNeg
                              theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_neg_infinitePos {x : ℝ*} {y : ℝ*} :
                              ¬x.Infinitesimalx < 0y.InfinitePos(x * y).InfiniteNeg
                              theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNeg¬y.Infinitesimal0 < y(x * y).InfiniteNeg
                              theorem Hyperreal.infiniteNeg_mul_of_not_infinitesimal_pos_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              ¬x.Infinitesimal0 < xy.InfiniteNeg(x * y).InfiniteNeg
                              theorem Hyperreal.infinitePos_mul_infinitePos {x : ℝ*} {y : ℝ*} :
                              x.InfinitePosy.InfinitePos(x * y).InfinitePos
                              theorem Hyperreal.infiniteNeg_mul_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNegy.InfiniteNeg(x * y).InfinitePos
                              theorem Hyperreal.infinitePos_mul_infiniteNeg {x : ℝ*} {y : ℝ*} :
                              x.InfinitePosy.InfiniteNeg(x * y).InfiniteNeg
                              theorem Hyperreal.infiniteNeg_mul_infinitePos {x : ℝ*} {y : ℝ*} :
                              x.InfiniteNegy.InfinitePos(x * y).InfiniteNeg
                              theorem Hyperreal.infinite_mul_of_infinite_not_infinitesimal {x : ℝ*} {y : ℝ*} :
                              x.Infinite¬y.Infinitesimal(x * y).Infinite
                              theorem Hyperreal.infinite_mul_of_not_infinitesimal_infinite {x : ℝ*} {y : ℝ*} :
                              ¬x.Infinitesimaly.Infinite(x * y).Infinite
                              theorem Hyperreal.Infinite.mul {x : ℝ*} {y : ℝ*} :
                              x.Infinitey.Infinite(x * y).Infinite