equal
deleted
inserted
replaced
1590 |
1590 |
1591 text \<open>Epsilon is a member of Infinitesimal.\<close> |
1591 text \<open>Epsilon is a member of Infinitesimal.\<close> |
1592 |
1592 |
1593 lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal" |
1593 lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal" |
1594 by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega |
1594 by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega |
1595 simp add: hypreal_epsilon_inverse_omega) |
1595 simp add: epsilon_inverse_omega) |
1596 |
1596 |
1597 lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite" |
1597 lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite" |
1598 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) |
1598 by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]) |
1599 |
1599 |
1600 lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0" |
1600 lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0" |