λδ digital library (LDDL)
Constant
Informal description: ""
{λ[r:real].λ[a0:dif].λ[a0ir:{((r).class).(a0)}.inn].λ[n:(r).neg]}.<({(0).(r)}.is).not>.{(λ[t:{(0).(r)}.is].{(t).(a0ir).(a0).(r)}.0ex).({({(n).(a0ir).(a0).(r)}.negex).(a0)}.nnot0d).((a0).zero).({(0).(r)}.is)}.th3 Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100