8000 minus of real x should be known to be at most abs(x) · Issue #22025 · sagemath/sage · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content
8000
minus of real x should be known to be at most abs(x) #22025
Open
@pelegm

Description

@pelegm

Check this:

sage: assume(x, 'real')
sage: bool(x <= abs(x))
True

but

sage: bool(-x <= abs(x))
False

and even

sage: bool(-x <= abs(-x))
False

(so this is a bit inconsistent).

Solve works here, but the set of solutions is not well simplified:

sage: solve(x <= abs(x), x)
#0: solve_rat_ineq(ineq=_SAGE_VAR_x <= abs(_SAGE_VAR_x))
[[x == 0], [0 < x], [x < 0]]
sage: solve(-x <= abs(x), x)
#0: solve_rat_ineq(ineq=-_SAGE_VAR_x <= abs(_SAGE_VAR_x))
[[x == 0], [x < 0], [0 < x]]

(so it also gives a debug message; see #22018)

Component: symbolics

Keywords: abs

Issue created by migration from https://trac.sagemath.org/ticket/22025

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions

      0