Function vstd::relations::is_greatest

source · 
pub open spec fn is_greatest<T>(leq: FnSpec<(T, T), bool>, max: T, s: Set<T>) -> bool
Expand description
{ s.contains(max) && forall |x: T| s.contains(x) ==> #[trigger] leq(x, max) }

An element in an ordered set is called a greatest element (or a maximum), if it is greater than every other element of the set.