Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
dedekind::category::IsBinaryFunction Concept Referenceexport
module dedekind.category

A binary relation R ⊆ A × B is a function when it is left-total AND right-unique. More...

Concept definition

template<typename R, typename A, typename B, typename Ω bool>
concept dedekind::category::IsBinaryFunction =
IsBinaryRelation<R, A, B, Ω> && is_left_total_v<std::remove_cvref_t<R>> &&
is_right_unique_v<std::remove_cvref_t<R>>
dedekind::category::IsBinaryFunction
A binary relation R ⊆ A × B is a function when it is left-total AND right-unique.
Definition cartesian.cppm:1028
dedekind::category::IsBinaryRelation
A type R is a binary relation A × B → bool if it is callable on A and B and yields a boolean.
Definition cartesian.cppm:975
dedekind::category::is_left_total_v
constexpr bool is_left_total_v
User-declared left-totality witness for a binary relation.
Definition cartesian.cppm:991
dedekind::category::is_right_unique_v
constexpr bool is_right_unique_v
User-declared right-uniqueness witness for a binary relation.
Definition cartesian.cppm:1001

Detailed Description

A binary relation R ⊆ A × B is a function when it is left-total AND right-unique.

The textbook function-as-relation characterisation: a function is a single-valued total relation. Combines IsBinaryRelation (structural shape) with the two opt-in honesty traits. Orthogonal classification axis to the posetal / equivalence axes (reflexive / symmetric / antisymmetric / transitive) in :mereology.