Interoperable interactive geometry for Europe
I forgot my login data
Register


Report a bug


Fan club

Quick Intro Videos
click to start movie
Create A Simple
GeoGebra Resource (25Mb)
click to start movie
Filing a review
click to start movie
Find a Resource

SPONSORS
This platform is brought to you by the intergeo project, funded under the eContent Plus programme of the European commission and by partners

end_point_of_directed_line_segment

Returns the end point of a line segment (that is, the second argument of its constructor).

Formal poperties

end_point_of_directed_line_segment(P,s), directed_line_segment_by_points(s,A,B) => P=B

(MH: the order of the antecedents seems to matter here, because there is scoping involved: s is only defined after directed_line_segment_by_points(s,A,B), so I would suggest to reverse the order)

MH:

A second possibility for formulation, given that we regard the symbols as being predicates, and therefore having a Boolean as output:

forall A,B in Points, forall s in Directed_Line_Segments, end_point_of_directed_line_segment(B,directed_line_segment_by_points(s,A,B))

Examples

  1. directed_line_segment example: source JSXGraph