The set of all tangent directions to the set s at the point x.

A property ensuring that the tangent cone to s at x spans a dense subset of the whole space. The main role of this property is to ensure that the differential within s at x is unique, hence this name. The uniqueness it asserts is proved in unique_diff_within_at.eq in deriv.lean. To avoid pathologies in dimension 0, we also require that x belongs to the closure of s (which is automatic when E is not 0-dimensional).

A property ensuring that the tangent cone to s at any of its points spans a dense subset of the whole space. The main role of this property is to ensure that the differential along s is unique, hence this name. The uniqueness it asserts is proved in unique_diff_on.eq in deriv.lean.

Auxiliary lemma ensuring that, under the assumptions defining the tangent cone, the sequence d tends to 0 at infinity.

Intersecting with a neighborhood of the point does not change the tangent cone.

The tangent cone of a product contains the tangent cone of its left factor.

The tangent cone of a product contains the tangent cone of its right factor.

If a subset of a real vector space contains a segment, then the direction of this segment belongs to the tangent cone at its endpoints.

The product of two sets of unique differentiability at points x and y has unique differentiability at (x, y).

The product of two sets of unique differentiability is a set of unique differentiability.

In a real vector space, a convex set with nonempty interior is a set of unique differentiability.

The real interval [0, 1] is a set of unique differentiability.