Function vstd::relations::is_least

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

An element in an ordered set is called a least element (or a minimum), if it is less than every other element of the set.

change f to leq bc it is a relation. also these are an ordering relation