Function vstd::relations::is_minimal

source · 
pub open spec fn is_minimal<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(x, min) ==> #[trigger] leq(min, x)
        }
}

An element in an ordered set is called a minimal element, if no other element is less than it.