Lines Matching refs:i2
1804 (!i1 i2. i1 IN iset /\ i2 IN iset /\ ~(i1 = i2)
1805 ==> (interior(i1) INTER interior(i2) = {}))
2020 (!i1 i2. i1 IN iset /\ i2 IN iset /\ ~(i1 = i2)
2021 ==> (interior(i1) INTER interior(i2) = {})) /\
4345 abs(s1 - i1) < e / &4:real /\ abs(s2 - i2) < e / &4:real
4346 ==> abs(i1 - i2) < e) /\
4360 abs(s1 - i1) < e / &4:real /\ abs(s2 - i2) < e / &4:real
4361 ==> abs(i1 - i2) < e)``,
6879 ``abs(i1 - i2) < e / &2 ==> abs(i1 - i) < e / &2 ==>
6880 abs(i2 - i) < e / &2 + e / &2:real``) THEN
10566 (X_CHOOSE_THEN ``i2:real->bool`` (X_CHOOSE_THEN ``l2:real->bool``
10571 ``((interior(i1) INTER interior(i2) = {}) \/
10574 interior(i2 INTER l2) SUBSET interior(i2) /\
10576 interior(i2 INTER l2) SUBSET interior(l2)
10577 ==> (interior(i1 INTER l1) INTER interior(i2 INTER l2) = {})``) THEN
10587 DISCH_THEN(MP_TAC o SPECL [``i1:real->bool``, ``i2:real->bool``]) THEN
16404 ``(i = i1 + i2)
16405 ==> abs(c + i1:real) <= abs(c) + abs(i) + abs(i2)``) THEN
17539 ``ga * (i1 + i2) + (gb - ga) * i2:real = ga * i1 + gb * i2:real``] THEN