s ⊂ t means that s is a strict subset of t, that is, s ⊆ t but s ≠ t.

The preimage of s : set β by f : α → β, written f ⁻¹' s, is the set of x : α such that f x ∈ s.

Two functions f₁ f₂ : α → β are equal on s if f₁ x = f₂ x for all x ∈ a.

A variant of image_comp, useful for rewriting

A variant of image_id

Range of a function.

This function is more flexible than f '' univ, as the image requires that the domain is in Type and not an arbitrary Sort.

The set s is pairwise r if r x y for all distinct x y ∈ s.

The cartesian product prod s t is the set of (a, b) such that a ∈ s and b ∈ t.

A product set is included in a product set if and only factors are included, or a factor of the first set is empty.

inclusion is the "identity" function between two subsets s and t, where s ⊆ t