Sets: Set-builder notation

The notation { element | predicate element } for the set of exactly those elements that satisfy a predicate, and the typed form { element : α | predicate element }.

Both forms mean MathlibMini.Set.ofPredicate fun element => .... The pretty printer shows ofPredicate applied to a function in set-builder form.

Inspired by Mathlib's Set. This is an independent, unofficial library.

def «term{_|_}» : Lean.ParserDescr

{ element | predicate } is the set of elements satisfying predicate.

Equations

• One or more equations did not get rendered due to their size.

def «term{_:_|_}» : Lean.ParserDescr

{ element : α | predicate } is the set of α satisfying predicate.

Equations

• One or more equations did not get rendered due to their size.

def MathlibMini.Set.unexpandOfPredicate : Lean.PrettyPrinter.Unexpander

Print ofPredicate fun element => predicate as { element | predicate }.

Equations

• One or more equations did not get rendered due to their size.

theorem MathlibMini.Set.mem_setOf_eq {α : Type u} {predicate : α → Prop} {element : α} : (element ∈ ofPredicate fun (x : α) => predicate x) = predicate element

Membership in a set-builder set is the predicate applied to the element. The simp lemma mem_ofPredicate_iff already covers this in simp.