ALEA.Prog_Intervals

Global Index

J

K

X

Y

_

(2841 entries)

Instance Index

E

G

H

J

K

Q

T

V

W

X

Y

Z

_

other

(149 entries)

Projection Index

A

B

G

H

J

K

Q

V

W

X

Y

Z

_

other

(50 entries)

Record Index

A

B

E

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(22 entries)

Lemma Index

J

K

V

X

Y

_

other

(1991 entries)

Section Index

A

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(35 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

(41 entries)

Constructor Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(17 entries)

Inductive Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Abbreviation Index

A

B

C

D

E

F

G

I

J

K

L

M

N

O

P

Q

S

T

U

W

X

Y

Z

_

other

(4 entries)

Definition Index

J

K

T

V

X

Y

_

other

(345 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(2 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(148 entries)

Library Index

A

E

F

G

H

J

K

L

N

O

Q

T

V

W

X

Y

Z

_

other

(22 entries)

R

Random [definition, in ALEA.Probas]
random [definition, in ALEA.Probas]
RandomList [library]
Random_inv [lemma, in ALEA.Probas]
Random_total [instance, in ALEA.Probas]
Random_simpl [lemma, in ALEA.Probas]
random_continuous [lemma, in ALEA.Probas]
random_stable_mult [lemma, in ALEA.Probas]
random_stable_plus [lemma, in ALEA.Probas]
random_stable_inv [lemma, in ALEA.Probas]
random_simpl [lemma, in ALEA.Probas]
random_mon [instance, in ALEA.Probas]
Random_eq [lemma, in ALEA.Cover]
Random_le [lemma, in ALEA.Cover]
Random_lt [lemma, in ALEA.Cover]
Random_carac [lemma, in ALEA.Cover]
random_fin_P [lemma, in ALEA.Cover]
random_fin_cover [lemma, in ALEA.Cover]
random_fin_total [lemma, in ALEA.Cover]
Random_fin_simpl [lemma, in ALEA.Cover]
Random_fin [definition, in ALEA.Cover]
random_fin_continuous [lemma, in ALEA.Cover]
random_fin_monotonic [lemma, in ALEA.Cover]
random_fin_stable_mult [lemma, in ALEA.Cover]
random_fin_stable_plus [lemma, in ALEA.Cover]
random_fin_stable_inv [lemma, in ALEA.Cover]
random_fin_simpl [lemma, in ALEA.Cover]
random_fin [definition, in ALEA.Cover]
range [definition, in ALEA.Prog]
range_le_compat [lemma, in ALEA.Prog]
range_impl [lemma, in ALEA.Prog]
range_eq [lemma, in ALEA.Prog]
range_le [lemma, in ALEA.Prog]
range_in_classes [lemma, in ALEA.IsDiscrete]
range_len [lemma, in ALEA.RandomList]
range_cover [lemma, in ALEA.Cover]
reflexive [projection, in ALEA.Ccpo]
rem [definition, in ALEA.Sets]
rem_incl [lemma, in ALEA.Sets]
rem_not_in [lemma, in ALEA.Sets]
rem_add_eqset_notin [lemma, in ALEA.Sets]
rem_eqset_notin [lemma, in ALEA.Sets]
rem_add_diff_eqset [lemma, in ALEA.Sets]
rem_add_eq_eqset [lemma, in ALEA.Sets]
retract [definition, in ALEA.Uprop]
retractS [lemma, in ALEA.Uprop]
retractS_intro [lemma, in ALEA.Uprop]
retractS_inv [lemma, in ALEA.Uprop]
retract_fplusok [lemma, in ALEA.Probas]
retract_zero_wretract [lemma, in ALEA.Uprop]
retract_wretract [lemma, in ALEA.Uprop]
retract_unif_Nnth [lemma, in ALEA.Uprop]
retract_unif [lemma, in ALEA.Uprop]
retract_lt [lemma, in ALEA.Uprop]
retract_pred [lemma, in ALEA.Uprop]
retract_class [lemma, in ALEA.Uprop]
retract_fin_le [lemma, in ALEA.Cover]
retract_fin_incl [lemma, in ALEA.Cover]
retract_fin_inv [lemma, in ALEA.Cover]
retract_fin [definition, in ALEA.Cover]
retract0 [lemma, in ALEA.Uprop]
Rp [record, in ALEA.Rplus]
Rpcompplus_mon [instance, in ALEA.Rplus]
Rpdiff_0_1 [lemma, in ALEA.Rplus]
Rpdistr_minus_left [lemma, in ALEA.Rplus]
Rpdistr_minus_right [lemma, in ALEA.Rplus]
Rpdistr_plus_left [lemma, in ALEA.Rplus]
Rpdistr_plus_right [lemma, in ALEA.Rplus]
Rpdiv [definition, in ALEA.Rplus]
Rpdiv_Rp1div [lemma, in ALEA.Rplus]
Rpdiv_le_compat [lemma, in ALEA.Rplus]
Rpeq [definition, in ALEA.Rplus]
Rpeq_dec [lemma, in ALEA.Rplus]
Rpeq_class [lemma, in ALEA.Rplus]
Rpeq_norm1 [lemma, in ALEA.Rplus]
Rpeq_norm [lemma, in ALEA.Rplus]
Rpeq_intro [lemma, in ALEA.Rplus]
Rpeq_simpl [lemma, in ALEA.Rplus]
RpExp [definition, in ALEA.Rplus]
Rpexp [definition, in ALEA.Rplus]
Rpexp_Rpmult_distr [lemma, in ALEA.Rplus]
Rpexp_Rpmult [lemma, in ALEA.Rplus]
Rpexp_Rp1div [lemma, in ALEA.Rplus]
Rpexp_Rp1div_left [lemma, in ALEA.Rplus]
Rpexp_Rp1div_right [lemma, in ALEA.Rplus]
Rpexp_one [lemma, in ALEA.Rplus]
Rpexp_zero [lemma, in ALEA.Rplus]
Rpexp_1 [lemma, in ALEA.Rplus]
Rpexp_0 [lemma, in ALEA.Rplus]
Rpexp_mon [instance, in ALEA.Rplus]
Rpexp_ge1_mon [lemma, in ALEA.Rplus]
Rpexp_le_compat [lemma, in ALEA.Rplus]
Rpexp_le1 [lemma, in ALEA.Rplus]
Rpexp_le1_mon [lemma, in ALEA.Rplus]
Rpexp_simpl [lemma, in ALEA.Rplus]
Rphalf_refl [lemma, in ALEA.Rplus]
Rphalf_plus [lemma, in ALEA.Rplus]
Rple [definition, in ALEA.Rplus]
Rple_lt_eps [lemma, in ALEA.Rplus]
Rple_plus_left [lemma, in ALEA.Rplus]
Rple_plus_right [lemma, in ALEA.Rplus]
Rple_S_N2Rp [lemma, in ALEA.Rplus]
Rple_floor [lemma, in ALEA.Rplus]
Rple_lt_dec [lemma, in ALEA.Rplus]
Rple_lt_eq_dec [lemma, in ALEA.Rplus]
Rple_dec [lemma, in ALEA.Rplus]
Rple_zero [lemma, in ALEA.Rplus]
Rple_total [lemma, in ALEA.Rplus]
Rple_class [lemma, in ALEA.Rplus]
Rple_N2Rp_mkRp [lemma, in ALEA.Rplus]
Rple_eq_floor_le_decimal [lemma, in ALEA.Rplus]
Rple_intro_le_floor [lemma, in ALEA.Rplus]
Rple_intro_eq [lemma, in ALEA.Rplus]
Rple_intro_lt [lemma, in ALEA.Rplus]
Rple_simpl [lemma, in ALEA.Rplus]
Rple1_U2Rp [lemma, in ALEA.Rplus]
Rplt_S_N2Rp [lemma, in ALEA.Rplus]
Rplt_nat_floor_lt [lemma, in ALEA.Rplus]
Rplt_nat_floor_le [lemma, in ALEA.Rplus]
Rplt_nat_floor [lemma, in ALEA.Rplus]
Rplt_neq_zero [lemma, in ALEA.Rplus]
Rplt_intro_lt_decimal [lemma, in ALEA.Rplus]
Rplt_intro_lt_floor [lemma, in ALEA.Rplus]
Rplt1_decimal [lemma, in ALEA.Rplus]
Rplt1_floor [lemma, in ALEA.Rplus]
Rplus [library]
RplusSFth [lemma, in ALEA.RpRing]
RplusSRmorph [lemma, in ALEA.RpRing]
RplusSRpowertheory [lemma, in ALEA.RpRing]
RplusSRth [lemma, in ALEA.RpRing]
Rpmin [definition, in ALEA.Rplus]
RpMinus [definition, in ALEA.Rplus]
Rpminus [definition, in ALEA.Rplus]
Rpminus_perm [lemma, in ALEA.Rplus]
Rpminus_assoc_left [lemma, in ALEA.Rplus]
Rpminus_Sn_1 [lemma, in ALEA.Rplus]
Rpminus_Sn_R1 [lemma, in ALEA.Rplus]
Rpminus_lt_0 [lemma, in ALEA.Rplus]
Rpminus_lt_compat_left [lemma, in ALEA.Rplus]
Rpminus_lt_compat_right [lemma, in ALEA.Rplus]
Rpminus_eq_perm_left [lemma, in ALEA.Rplus]
Rpminus_eq_perm_right [lemma, in ALEA.Rplus]
Rpminus_le_perm_left [lemma, in ALEA.Rplus]
Rpminus_le_perm_right [lemma, in ALEA.Rplus]
Rpminus_zero_le [lemma, in ALEA.Rplus]
Rpminus_assoc_right [lemma, in ALEA.Rplus]
Rpminus_plus_perm [lemma, in ALEA.Rplus]
Rpminus_plus_perm_right [lemma, in ALEA.Rplus]
Rpminus_plus_simpl_le [lemma, in ALEA.Rplus]
Rpminus_plus_simpl [lemma, in ALEA.Rplus]
Rpminus_eq [lemma, in ALEA.Rplus]
Rpminus_zero_left [lemma, in ALEA.Rplus]
Rpminus_mon2 [instance, in ALEA.Rplus]
Rpminus_le_compat [lemma, in ALEA.Rplus]
Rpminus_eq_compat [lemma, in ALEA.Rplus]
Rpminus_eq_compat_right [lemma, in ALEA.Rplus]
Rpminus_le_compat_right [lemma, in ALEA.Rplus]
Rpminus_eq_compat_left [lemma, in ALEA.Rplus]
Rpminus_le_compat_left [lemma, in ALEA.Rplus]
Rpminus_zero_right [lemma, in ALEA.Rplus]
Rpminus_le_zero [lemma, in ALEA.Rplus]
Rpminus_simpl_gtc2 [lemma, in ALEA.Rplus]
Rpminus_simpl_gtc [lemma, in ALEA.Rplus]
Rpminus_simpl_gt2 [lemma, in ALEA.Rplus]
Rpminus_simpl_gt [lemma, in ALEA.Rplus]
Rpminus_simpl_eq [lemma, in ALEA.Rplus]
Rpminus_simpl_lt [lemma, in ALEA.Rplus]
Rpminus_rec [lemma, in ALEA.Rplus]
Rpmin_eq_left [lemma, in ALEA.Rplus]
Rpmin_eq_right [lemma, in ALEA.Rplus]
Rpmin_idem [lemma, in ALEA.Rplus]
Rpmin_le_compat_right [lemma, in ALEA.Rplus]
Rpmin_le_compat_left [lemma, in ALEA.Rplus]
Rpmin_sym [lemma, in ALEA.Rplus]
Rpmin_le_sym [lemma, in ALEA.Rplus]
Rpmin_le [lemma, in ALEA.Rplus]
Rpmin_le_left [lemma, in ALEA.Rplus]
Rpmin_le_right [lemma, in ALEA.Rplus]
RpMult [definition, in ALEA.Rplus]
Rpmult [definition, in ALEA.Rplus]
Rpmult_Rp1div [lemma, in ALEA.Rplus]
Rpmult_lt_zero [lemma, in ALEA.Rplus]
Rpmult_eq_perm_left [lemma, in ALEA.Rplus]
Rpmult_le_perm_left [lemma, in ALEA.Rplus]
Rpmult_eq_perm_right [lemma, in ALEA.Rplus]
Rpmult_le_perm_right [lemma, in ALEA.Rplus]
Rpmult_eq_simpl_right [lemma, in ALEA.Rplus]
Rpmult_eq_simpl_left [lemma, in ALEA.Rplus]
Rpmult_le_simpl_right [lemma, in ALEA.Rplus]
Rpmult_le_simpl_left [lemma, in ALEA.Rplus]
Rpmult_not_0 [lemma, in ALEA.Rplus]
Rpmult_0_simpl [lemma, in ALEA.Rplus]
Rpmult_not0_right [lemma, in ALEA.Rplus]
Rpmult_not0_left [lemma, in ALEA.Rplus]
Rpmult_one_right [lemma, in ALEA.Rplus]
Rpmult_assoc [lemma, in ALEA.Rplus]
Rpmult_decomp [lemma, in ALEA.Rplus]
Rpmult_NRpmult_perm [lemma, in ALEA.Rplus]
Rpmult_mon2 [instance, in ALEA.Rplus]
Rpmult_eq_compat_right [lemma, in ALEA.Rplus]
Rpmult_eq_compat_left [lemma, in ALEA.Rplus]
Rpmult_le_compat_right [lemma, in ALEA.Rplus]
Rpmult_le_compat_left [lemma, in ALEA.Rplus]
Rpmult_stable2 [instance, in ALEA.Rplus]
Rpmult_monotonic2 [instance, in ALEA.Rplus]
Rpmult_mon_right [instance, in ALEA.Rplus]
Rpmult_one_left [lemma, in ALEA.Rplus]
Rpmult_zero_right [lemma, in ALEA.Rplus]
Rpmult_sym [lemma, in ALEA.Rplus]
Rpmult_zero_left [lemma, in ALEA.Rplus]
Rpmult2_decomp [lemma, in ALEA.Rplus]
Rpord [instance, in ALEA.Rplus]
RpPlus [definition, in ALEA.Rplus]
Rpplus [definition, in ALEA.Rplus]
Rpplus_0_simpl [lemma, in ALEA.Rplus]
Rpplus_0_simpl_right [lemma, in ALEA.Rplus]
Rpplus_0_simpl_left [lemma, in ALEA.Rplus]
Rpplus_lt_simpl_right [lemma, in ALEA.Rplus]
Rpplus_lt_simpl_left [lemma, in ALEA.Rplus]
Rpplus_Uinv_le [lemma, in ALEA.Rplus]
Rpplus_lt_compat_right [lemma, in ALEA.Rplus]
Rpplus_lt_compat_left [lemma, in ALEA.Rplus]
Rpplus_minus_assoc [lemma, in ALEA.Rplus]
Rpplus_le_perm_right [lemma, in ALEA.Rplus]
Rpplus_le_perm_left [lemma, in ALEA.Rplus]
Rpplus_eq_perm_right [lemma, in ALEA.Rplus]
Rpplus_eq_perm_left [lemma, in ALEA.Rplus]
Rpplus_eq_simpl_left [lemma, in ALEA.Rplus]
Rpplus_eq_simpl_right [lemma, in ALEA.Rplus]
Rpplus_le_simpl_left [lemma, in ALEA.Rplus]
Rpplus_le_simpl_right [lemma, in ALEA.Rplus]
Rpplus_minus_simpl_left [lemma, in ALEA.Rplus]
Rpplus_minus_simpl_right [lemma, in ALEA.Rplus]
Rpplus_perm2 [lemma, in ALEA.Rplus]
Rpplus_perm3 [lemma, in ALEA.Rplus]
Rpplus_mon2 [instance, in ALEA.Rplus]
Rpplus_eq_compat_right [lemma, in ALEA.Rplus]
Rpplus_eq_compat_left [lemma, in ALEA.Rplus]
Rpplus_le_compat_right [lemma, in ALEA.Rplus]
Rpplus_le_compat_left [lemma, in ALEA.Rplus]
Rpplus_monotonic2 [instance, in ALEA.Rplus]
Rpplus_mon_right [instance, in ALEA.Rplus]
Rpplus_NU2Rp [lemma, in ALEA.Rplus]
Rpplus_floor_decimal [lemma, in ALEA.Rplus]
Rpplus_assoc [lemma, in ALEA.Rplus]
Rpplus_zero_right [lemma, in ALEA.Rplus]
Rpplus_zero_left [lemma, in ALEA.Rplus]
Rpplus_sym [lemma, in ALEA.Rplus]
Rpplus_simpl_ok2 [lemma, in ALEA.Rplus]
Rpplus_simpl_over [lemma, in ALEA.Rplus]
Rpplus_simpl_ok [lemma, in ALEA.Rplus]
Rpplus_rec [lemma, in ALEA.Rplus]
Rpplus_simpl [lemma, in ALEA.Rplus]
RpRing [library]
Rpsigma [definition, in ALEA.Rplus]
Rpsigma_U2Rp_bound [lemma, in ALEA.Rplus]
Rpsigma_U2Rp [lemma, in ALEA.Rplus]
Rpsigma_mult [lemma, in ALEA.Rplus]
Rpsigma_plus [lemma, in ALEA.Rplus]
Rpsigma_mon [instance, in ALEA.Rplus]
Rpsigma_minus_incr [lemma, in ALEA.Rplus]
Rpsigma_minus_decr [lemma, in ALEA.Rplus]
Rpsigma_zero_elim [lemma, in ALEA.Rplus]
Rpsigma_not_zero [lemma, in ALEA.Rplus]
Rpsigma_le [lemma, in ALEA.Rplus]
Rpsigma_zero [lemma, in ALEA.Rplus]
Rpsigma_plus_lift [lemma, in ALEA.Rplus]
Rpsigma_S_lift [lemma, in ALEA.Rplus]
Rpsigma_eq_compat_index [lemma, in ALEA.Rplus]
Rpsigma_eq_compat [lemma, in ALEA.Rplus]
Rpsigma_le_compat [lemma, in ALEA.Rplus]
Rpsigma_incr [lemma, in ALEA.Rplus]
Rpsigma_1 [lemma, in ALEA.Rplus]
Rpsigma_S [lemma, in ALEA.Rplus]
Rpsigma_0 [lemma, in ALEA.Rplus]
Rp_lt_eq_lt_dec [lemma, in ALEA.Rplus]
Rp1div [definition, in ALEA.Rplus]
Rp1div_lt_compat [lemma, in ALEA.Rplus]
Rp1div_eq_simpl [lemma, in ALEA.Rplus]
Rp1div_le_simpl [lemma, in ALEA.Rplus]
Rp1div_Rp1div [lemma, in ALEA.Rplus]
Rp1div_1 [lemma, in ALEA.Rplus]
Rp1div_le_compat [lemma, in ALEA.Rplus]
Rp1div_eq_perm_right [lemma, in ALEA.Rplus]
Rp1div_le_perm_right [lemma, in ALEA.Rplus]
Rp1div_eq_perm_left [lemma, in ALEA.Rplus]
Rp1div_le_perm_left [lemma, in ALEA.Rplus]
Rp1div_0 [lemma, in ALEA.Rplus]
Rp1div_zero [lemma, in ALEA.Rplus]
Rp1div_right [lemma, in ALEA.Rplus]
Rp1div_left [lemma, in ALEA.Rplus]
Rp1div_def.a [variable, in ALEA.Rplus]
Rp1div_def.x [variable, in ALEA.Rplus]
Rp1div_def [section, in ALEA.Rplus]
R0 [abbreviation, in ALEA.Rplus]
R1 [abbreviation, in ALEA.Rplus]

Global Index

J

K

X

Y

_

(2841 entries)

Instance Index

E

G

H

J

K

Q

T

V

W

X

Y

Z

_

other

(149 entries)

Projection Index

A

B

G

H

J

K

Q

V

W

X

Y

Z

_

other

(50 entries)

Record Index

A

B

E

G

H

J

K

L

P

Q

U

V

W

X

Y

Z

_

other

(22 entries)

Lemma Index

J

K

V

X

Y

_

other

(1991 entries)

Section Index

A

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(35 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

(41 entries)

Constructor Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(17 entries)

Inductive Index

A

B

D

E

G

H

I

J

K

L

O

P

Q

R

U

V

W

X

Y

Z

_

other

(9 entries)

Abbreviation Index

A

B

C

D

E

F

G

I

J

K

L

M

N

O

P

Q

S

T

U

W

X

Y

Z

_

other

(4 entries)

Definition Index

J

K

T

V

X

Y

_

other

(345 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(2 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(6 entries)

Variable Index

B

E

H

J

K

M

N

O

Q

V

X

Y

Z

_

other

(148 entries)

Library Index

A

E

F

G

H

J

K

L

N

O

Q

T

V

W

X

Y

Z

_

other

(22 entries)