Skip to content

Commit e2778f0

Browse files
jdyeagerJared Yeager
jdyeager
and
Jared Yeager
authored
Hyperbolic Trigonometry (#1606)
A healthy number of results concerning hyperbolic trigonometry. This includes results added to realScript, real_topologyScript, and limScript to support results in transcScript. * Lemmas about reals in prep for hyperbolic trig. * Lemmas in real topology for hyperbolic trig prep. * Derivative stuff in limScript as hyper_trig prep. * Hyperbolic trigonometry library * Moving things around * Putting the booleanresult in trans theory --------- Co-authored-by: Jared Yeager <[email protected]>
1 parent e230e5b commit e2778f0

File tree

4 files changed

+1660
-1
lines changed

4 files changed

+1660
-1
lines changed

‎src/real/analysis/limScript.sml‎

Lines changed: 260 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1730,3 +1730,263 @@ Proof
17301730
ASM_SIMP_TAC std_ss [DIFF_NEG]
17311731
QED
17321732

1733+
(*---------------------------------------------------------------------------*)
1734+
(* Miscellaneous Results (for use in hyperbolic trigonemtry library) *)
1735+
(*---------------------------------------------------------------------------*)
1736+
1737+
Theorem DIFF_CONG:
1738+
∀f g l m x y. (∃a b. a < y ∧ y < b ∧ ∀z. a < z ∧ z < b ⇒ (f z = g z)) ∧
1739+
(l = m) ∧ (x = y) ⇒ ((f diffl l) x ⇔ (g diffl m) y)
1740+
Proof
1741+
simp[] >>
1742+
‘∀f g m y. (∃a b. a < y ∧ y < b ∧ ∀z. a < z ∧ z < b ⇒ (f z = g z)) ∧
1743+
(f diffl m) y ⇒ (g diffl m) y’ suffices_by metis_tac[] >>
1744+
rw[] >> pop_assum mp_tac >> simp[diffl,LIM] >> rw[] >>
1745+
first_x_assum $ drule_then assume_tac >> gs[] >>
1746+
qexists ‘min d (min (y - a) (b - y))’ >> simp[REAL_LT_MIN,REAL_SUB_LT] >> rw[] >>
1747+
first_x_assum $ drule_all_then mp_tac >>
1748+
‘f (y + h) = g (y + h)’ suffices_by simp[] >> first_x_assum irule >>
1749+
gs[ABS_BOUNDS_LT,REAL_NEG_SUB,REAL_LT_SUB_LADD,REAL_LT_SUB_RADD] >>
1750+
simp[REAL_ADD_COMM]
1751+
QED
1752+
1753+
Theorem DIFF_POS_MONO_LT_INTERVAL:
1754+
∀f s. is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧
1755+
(∀z. z ∈ interior s ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1756+
∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ f x < f y
1757+
Proof
1758+
rw[] >>
1759+
‘∀z. x < z ∧ z < y ⇒ z ∈ interior s’ by (
1760+
rw[interior] >> qexists ‘interval (x,y)’ >> simp[OPEN_INTERVAL] >>
1761+
gs[SUBSET_DEF,OPEN_interval,IS_INTERVAL] >> metis_tac[REAL_LE_LT]) >>
1762+
qspecl_then [‘f’,‘x’,‘y’] mp_tac MVT >> impl_tac
1763+
>- (gs[IS_INTERVAL] >> metis_tac[differentiable]) >>
1764+
rw[] >> pop_assum mp_tac >> simp[REAL_EQ_SUB_RADD] >> disch_then kall_tac >>
1765+
irule REAL_LT_MUL >> simp[REAL_SUB_LT] >>
1766+
ntac 2 $ first_x_assum $ dxrule_all_then assume_tac >> metis_tac[DIFF_UNIQ]
1767+
QED
1768+
1769+
Theorem DIFF_NEG_ANTIMONO_LT_INTERVAL:
1770+
∀f s. is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧
1771+
(∀z. z ∈ interior s ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1772+
∀x y. x ∈ s ∧ y ∈ s ∧ x < y ⇒ f y < f x
1773+
Proof
1774+
rw[] >> qspecl_then [‘λw. -f w’,‘s’] mp_tac DIFF_POS_MONO_LT_INTERVAL >>
1775+
simp[] >> disch_then irule >> simp[CONT_NEG] >> rw[] >>
1776+
first_x_assum $ dxrule_then assume_tac >> gs[] >>
1777+
qexists ‘-l’ >> simp[DIFF_NEG]
1778+
QED
1779+
1780+
Theorem DIFF_POS_MONO_LT_UU:
1781+
∀f. (∀z. ∃l. 0 < l ∧ (f diffl l) z) ⇒
1782+
∀x y. x < y ⇒ f x < f y
1783+
Proof
1784+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1785+
qexists ‘𝕌(:real)’ >> simp[IS_INTERVAL_POSSIBILITIES] >>
1786+
metis_tac[DIFF_CONT]
1787+
QED
1788+
1789+
Theorem DIFF_POS_MONO_LT_OU:
1790+
∀f a. (∀z. a < z ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1791+
∀x y. a < x ∧ x < y ⇒ f x < f y
1792+
Proof
1793+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1794+
qexists ‘{x | a < x}’ >>
1795+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1796+
metis_tac[DIFF_CONT]
1797+
QED
1798+
1799+
Theorem DIFF_POS_MONO_LT_UO:
1800+
∀f b. (∀z. z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1801+
∀x y. y < b ∧ x < y ⇒ f x < f y
1802+
Proof
1803+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1804+
qexists ‘{x | x < b}’ >>
1805+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1806+
metis_tac[DIFF_CONT]
1807+
QED
1808+
1809+
Theorem DIFF_POS_MONO_LT_CU:
1810+
∀f a. f contl a ∧ (∀z. a < z ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1811+
∀x y. a ≤ x ∧ x < y ⇒ f x < f y
1812+
Proof
1813+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1814+
qexists ‘{x | a ≤ x}’ >>
1815+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1816+
metis_tac[DIFF_CONT,REAL_LE_LT]
1817+
QED
1818+
1819+
Theorem DIFF_POS_MONO_LT_UC:
1820+
∀f b. f contl b ∧ (∀z. z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1821+
∀x y. y ≤ b ∧ x < y ⇒ f x < f y
1822+
Proof
1823+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1824+
qexists ‘{x | x ≤ b}’ >>
1825+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1826+
metis_tac[DIFF_CONT,REAL_LE_LT]
1827+
QED
1828+
1829+
Theorem DIFF_POS_MONO_LT_OO:
1830+
∀f a b. (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1831+
∀x y. a < x ∧ y < b ∧ x < y ⇒ f x < f y
1832+
Proof
1833+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1834+
qexists ‘{x | a < x ∧ x < b}’ >>
1835+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1836+
metis_tac[DIFF_CONT]
1837+
QED
1838+
1839+
Theorem DIFF_POS_MONO_LT_CO:
1840+
∀f a b. f contl a ∧ (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1841+
∀x y. a ≤ x ∧ y < b ∧ x < y ⇒ f x < f y
1842+
Proof
1843+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1844+
qexists ‘{x | a ≤ x ∧ x < b}’ >>
1845+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1846+
REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1847+
metis_tac[DIFF_CONT,REAL_LE_LT]
1848+
QED
1849+
1850+
Theorem DIFF_POS_MONO_LT_OC:
1851+
∀f a b. f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1852+
∀x y. a < x ∧ y ≤ b ∧ x < y ⇒ f x < f y
1853+
Proof
1854+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1855+
qexists ‘{x | a < x ∧ x ≤ b}’ >>
1856+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1857+
REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1858+
metis_tac[DIFF_CONT,REAL_LE_LT]
1859+
QED
1860+
1861+
Theorem DIFF_POS_MONO_LT_CC:
1862+
∀f a b. f contl a ∧ f contl b ∧
1863+
(∀z. a < z ∧ z < b ⇒ ∃l. 0 < l ∧ (f diffl l) z) ⇒
1864+
∀x y. a ≤ x ∧ y ≤ b ∧ x < y ⇒ f x < f y
1865+
Proof
1866+
rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1867+
qexists ‘{x | a ≤ x ∧ x ≤ b}’ >>
1868+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1869+
REAL_LT_IMP_LE,REAL_LET_TRANS,REAL_LTE_TRANS,SF SFY_ss] >>
1870+
metis_tac[DIFF_CONT,REAL_LE_LT]
1871+
QED
1872+
1873+
Theorem DIFF_NEG_ANTIMONO_LT_UU:
1874+
∀f. (∀z. ∃l. l < 0 ∧ (f diffl l) z) ⇒
1875+
∀x y. x < y ⇒ f y < f x
1876+
Proof
1877+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1878+
qexists ‘𝕌(:real)’ >> simp[IS_INTERVAL_POSSIBILITIES] >>
1879+
metis_tac[DIFF_CONT]
1880+
QED
1881+
1882+
Theorem DIFF_NEG_ANTIMONO_LT_OU:
1883+
∀f a. (∀z. a < z ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1884+
∀x y. a < x ∧ x < y ⇒ f y < f x
1885+
Proof
1886+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1887+
qexists ‘{x | a < x}’ >>
1888+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1889+
metis_tac[DIFF_CONT]
1890+
QED
1891+
1892+
Theorem DIFF_NEG_ANTIMONO_LT_UO:
1893+
∀f b. (∀z. z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1894+
∀x y. y < b ∧ x < y ⇒ f y < f x
1895+
Proof
1896+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1897+
qexists ‘{x | x < b}’ >>
1898+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1899+
metis_tac[DIFF_CONT]
1900+
QED
1901+
1902+
Theorem DIFF_NEG_ANTIMONO_LT_CU:
1903+
∀f a. f contl a ∧ (∀z. a < z ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1904+
∀x y. a ≤ x ∧ x < y ⇒ f y < f x
1905+
Proof
1906+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1907+
qexists ‘{x | a ≤ x}’ >>
1908+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1909+
metis_tac[DIFF_CONT,REAL_LE_LT]
1910+
QED
1911+
1912+
Theorem DIFF_NEG_ANTIMONO_LT_UC:
1913+
∀f b. f contl b ∧ (∀z. z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1914+
∀x y. y ≤ b ∧ x < y ⇒ f y < f x
1915+
Proof
1916+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1917+
qexists ‘{x | x ≤ b}’ >>
1918+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1919+
metis_tac[DIFF_CONT,REAL_LE_LT]
1920+
QED
1921+
1922+
Theorem DIFF_NEG_ANTIMONO_LT_OO:
1923+
∀f a b. (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1924+
∀x y. a < x ∧ y < b ∧ x < y ⇒ f y < f x
1925+
Proof
1926+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1927+
qexists ‘{x | a < x ∧ x < b}’ >>
1928+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1929+
metis_tac[DIFF_CONT]
1930+
QED
1931+
1932+
Theorem DIFF_NEG_ANTIMONO_LT_CO:
1933+
∀f a b. f contl a ∧ (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1934+
∀x y. a ≤ x ∧ y < b ∧ x < y ⇒ f y < f x
1935+
Proof
1936+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1937+
qexists ‘{x | a ≤ x ∧ x < b}’ >>
1938+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1939+
REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1940+
metis_tac[DIFF_CONT,REAL_LE_LT]
1941+
QED
1942+
1943+
Theorem DIFF_NEG_ANTIMONO_LT_OC:
1944+
∀f a b. f contl b ∧ (∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1945+
∀x y. a < x ∧ y ≤ b ∧ x < y ⇒ f y < f x
1946+
Proof
1947+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1948+
qexists ‘{x | a < x ∧ x ≤ b}’ >>
1949+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1950+
REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1951+
metis_tac[DIFF_CONT,REAL_LE_LT]
1952+
QED
1953+
1954+
Theorem DIFF_NEG_ANTIMONO_LT_CC:
1955+
∀f a b. f contl a ∧ f contl b ∧
1956+
(∀z. a < z ∧ z < b ⇒ ∃l. l < 0 ∧ (f diffl l) z) ⇒
1957+
∀x y. a ≤ x ∧ y ≤ b ∧ x < y ⇒ f y < f x
1958+
Proof
1959+
rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1960+
qexists ‘{x | a ≤ x ∧ x ≤ b}’ >>
1961+
simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1962+
REAL_LT_IMP_LE,REAL_LET_TRANS,REAL_LTE_TRANS,SF SFY_ss] >>
1963+
metis_tac[DIFF_CONT,REAL_LE_LT]
1964+
QED
1965+
1966+
Theorem DIFF_EQ_FUN_EQ:
1967+
∀f g s. is_interval s ∧ (∀z. z ∈ s ⇒ f contl z) ∧ (∀z. z ∈ s ⇒ g contl z) ∧
1968+
(∀z. z ∈ interior s ⇒ ∃l. (f diffl l) z ∧ (g diffl l) z) ⇒
1969+
∃c. ∀x. x ∈ s ⇒ (f x = g x + c)
1970+
Proof
1971+
rw[] >> Cases_on ‘s = ∅’ >- simp[] >>
1972+
gs[GSYM MEMBER_NOT_EMPTY] >> rename [‘w ∈ s’] >>
1973+
qexists ‘f w - g w’ >> rw[] >>
1974+
‘f x - g x = f w - g w’ suffices_by (
1975+
simp[REAL_EQ_SUB_RADD,real_sub,REAL_ADD_ASSOC] >>
1976+
disch_then kall_tac >> metis_tac[REAL_ADD_COMM,REAL_ADD_ASSOC]) >>
1977+
Cases_on ‘x = w’ >- simp[] >> wlog_tac ‘w < x’ [‘x’,‘w’]
1978+
>- (first_x_assum $ qspecl_then [‘w’,‘x’] mp_tac >> simp[] >>
1979+
‘x < w’ suffices_by simp[] >> gs[REAL_NOT_LT,REAL_LE_LT]) >>
1980+
‘∀z. z ∈ s ⇒ (λx. f x − g x) contl z’ by simp[CONT_SUB] >>
1981+
‘∀z. z ∈ interior s ⇒ ((λx. f x − g x) diffl 0) z’ by (
1982+
rw[] >> qpat_x_assum ‘∀z. z ∈ interior s ⇒ _’ $ dxrule_then assume_tac >>
1983+
gs[] >> qspecl_then [‘f’,‘g’,‘l’,‘l’,‘z’] mp_tac DIFF_SUB >> simp[]) >>
1984+
‘∀z. w < z ∧ z < x ⇒ z ∈ interior s’ by (rw[interior] >>
1985+
qexists ‘interval (w,x)’ >> simp[OPEN_INTERVAL,OPEN_interval,SUBSET_DEF] >>
1986+
metis_tac[REAL_LE_LT,IS_INTERVAL]) >>
1987+
qspecl_then [‘λx. f x - g x’,‘w’,‘x’] mp_tac MVT >> simp[] >> impl_tac
1988+
>- (conj_tac >- metis_tac[IS_INTERVAL] >> qx_gen_tac ‘y’ >> strip_tac >>
1989+
simp[differentiable] >> first_x_assum $ irule_at Any >> simp[]) >>
1990+
rw[] >> ntac 2 $ first_x_assum $ dxrule_all_then assume_tac >>
1991+
dxrule_all_then assume_tac DIFF_UNIQ >> rw[] >> gs[REAL_MUL_LZERO]
1992+
QED

‎src/real/analysis/real_topologyScript.sml‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14449,6 +14449,21 @@ val IS_INTERVAL_CASES = store_thm ("IS_INTERVAL_CASES",
1444914449
REWRITE_TAC[GSYM REAL_NOT_LE] THEN
1445014450
ASM_MESON_TAC [REAL_LE_TRANS, REAL_LE_TOTAL, REAL_LE_ANTISYM]);
1445114451

14452+
Theorem IS_INTERVAL_POSSIBILITIES:
14453+
(is_interval ∅) ∧
14454+
(is_interval 𝕌(:real)) ∧
14455+
(∀a. is_interval {x | a ≤ x}) ∧
14456+
(∀a. is_interval {x | a < x}) ∧
14457+
(∀b. is_interval {x | x ≤ b}) ∧
14458+
(∀b. is_interval {x | x < b}) ∧
14459+
(∀a b. is_interval {x | a ≤ x ∧ x ≤ b}) ∧
14460+
(∀a b. is_interval {x | a ≤ x ∧ x < b}) ∧
14461+
(∀a b. is_interval {x | a < x ∧ x ≤ b}) ∧
14462+
(∀a b. is_interval {x | a < x ∧ x < b})
14463+
Proof
14464+
metis_tac[IS_INTERVAL_CASES]
14465+
QED
14466+
1445214467
val IS_INTERVAL_INTER = store_thm ("IS_INTERVAL_INTER",
1445314468
``!s t:real->bool.
1445414469
is_interval s /\ is_interval t ==> is_interval(s INTER t)``,
@@ -14691,6 +14706,28 @@ val CARD_FRONTIER_INTERVAL = store_thm ("CARD_FRONTIER_INTERVAL",
1469114706
ASM_REWRITE_TAC[] THEN FULL_SIMP_TAC std_ss [REAL_LT_RDIV_EQ, REAL_ARITH ``0 < 2:real``] THEN
1469214707
ASM_REAL_ARITH_TAC);
1469314708

14709+
Theorem INTERIOR_INTERVAL_CASES:
14710+
(interior ∅ = ∅) ∧
14711+
(interior 𝕌(:real) = 𝕌(:real)) ∧
14712+
(∀a. interior {x | a ≤ x} = {x | a < x}) ∧
14713+
(∀a. interior {x | a < x} = {x | a < x}) ∧
14714+
(∀b. interior {x | x ≤ b} = {x | x < b}) ∧
14715+
(∀b. interior {x | x < b} = {x | x < b}) ∧
14716+
(∀a b. interior {x | a ≤ x ∧ x ≤ b} = {x | a < x ∧ x < b}) ∧
14717+
(∀a b. interior {x | a ≤ x ∧ x < b} = {x | a < x ∧ x < b}) ∧
14718+
(∀a b. interior {x | a < x ∧ x ≤ b} = {x | a < x ∧ x < b}) ∧
14719+
(∀a b. interior {x | a < x ∧ x < b} = {x | a < x ∧ x < b})
14720+
Proof
14721+
simp[SRULE [CLOSED_interval,OPEN_interval] INTERIOR_INTERVAL] >>
14722+
‘∀a b. {x | a ≤ x ∧ x < b} = {x | a ≤ x} ∩ {x | x < b}’ by simp[EXTENSION] >>
14723+
‘∀a b. {x | a < x ∧ x ≤ b} = {x | a < x} ∩ {x | x ≤ b}’ by simp[EXTENSION] >>
14724+
‘∀a b. {x | a < x ∧ x < b} = {x | a < x} ∩ {x | x < b}’ by simp[EXTENSION] >>
14725+
csimp[INTERIOR_INTER] >>
14726+
simp[INTERIOR_EMPTY,INTERIOR_UNIV,INTERIOR_HALFSPACE_COMPONENT_LE,
14727+
SRULE [real_ge,real_gt] INTERIOR_HALFSPACE_COMPONENT_GE] >>
14728+
simp[INTERIOR_EQ,OPEN_INTERVAL_RIGHT,OPEN_INTERVAL_LEFT]
14729+
QED
14730+
1469414731
(* ------------------------------------------------------------------------- *)
1469514732
(* Limit component bounds. *)
1469614733
(* ------------------------------------------------------------------------- *)

0 commit comments

Comments
 (0)