Subtype p, usually written as {x : α // p x}, is a type which
represents all the elements x : α for which p x is true. It is structurally
a pair-like type, so if you have x : α and h : p x then
⟨x, h⟩ : {x // p x}. An element s : {x // p x} will coerce to α but
you can also make it explicit using s.1 or s.val.
Constructor
Subtype.mk.{u}
Fields
val : α
If s : {x // p x} then s.val : α is the underlying element in the base
type. You can also write this as s.1, or simply as s when the type is
known from context.
property : p self.val
If s : {x // p x} then s.2 or s.property is the assertion that
p s.1, that is, that s is in fact an element for which p holds.