CurrentElectrons
includes
FermiPotentialElectrons
includes
ElectrostaticPotential
includes
DensityElectrons
includes
Mobilities
constant
current_electrons
Show Notations
Languages
Arguments
Rendering
3
j_n
a
b
c
[
P
:
ℝ
→
bool
]
(
[
f
:
(
pred_as_sub
P
)
→
ℝ
,
g
:
(
pred_as_sub
P
)
→
ℝ
]
(
[
x
:
pred_as_sub
P
]
(
multiplication
(
multiplication
(
multiplication
(
uminus
q
)
μ_n
)
(
n
(
f
x
)
(
g
x
)
)
)
(
(
der
(
[
z
:
ℝ
]
(
P
z
)
)
g
)
x
)
)
)
)
http://cds.omdoc.org/urtheories?LambdaPi?lambda
P
http://cds.omdoc.org/urtheories?LambdaPi?arrow
http://mathhub.info/MitM/numberfields?realnumbers?Realnumbers
http://mathhub.info/MitM/Foundation?Logic?bool
http://cds.omdoc.org/urtheories?LambdaPi?lambda
f
http://cds.omdoc.org/urtheories?LambdaPi?arrow
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?pred_as_sub
P
http://mathhub.info/MitM/numberfields?realnumbers?Realnumbers
g
http://cds.omdoc.org/urtheories?LambdaPi?arrow
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?pred_as_sub
P
http://mathhub.info/MitM/numberfields?realnumbers?Realnumbers
http://cds.omdoc.org/urtheories?LambdaPi?lambda
x
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?pred_as_sub
P
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?multiplication
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?multiplication
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?multiplication
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/numberfields?realarith?uminus
http://mathhub.info/MitM/Models?PhysicalConstants?elementary_charge
http://mathhub.info/MitM/Models/continuity?Mobilities?mobility_electrons
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/Models/densities?DensityElectrons?density_electrons
http://cds.omdoc.org/urtheories?LambdaPi?apply
f
x
http://cds.omdoc.org/urtheories?LambdaPi?apply
g
x
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://cds.omdoc.org/urtheories?LambdaPi?apply
http://mathhub.info/MitM/Models?Base?der
http://cds.omdoc.org/urtheories?LambdaPi?lambda
z
http://mathhub.info/MitM/numberfields?realnumbers?Realnumbers
http://cds.omdoc.org/urtheories?LambdaPi?apply
P
z
g
x