λδ digital library (LDDL)
Constant
Informal description: ""
{λ[r:real].λ[s:real].λ[p:(r).pos].λ[q:(s).pos]}.<{({((s).abs).((r).abs)}.ts).({(s).(r)}.ts)}.is>.{({({(q).(s)}.absp).({(p).(r)}.absp).(s).((s).abs).(r).((r).abs)}.ists12).({(s).(r)}.ts).({((s).abs).((r).abs)}.ts).(real)}.symis Validation parameters: sort hierarchy = "Z2", kernel options = ""
Last update: Sat, 12 Dec 2020 10:46:54 +0100