mathlib3

350ba8db - feat(data/two_pointing): Two pointings of a type (#11648)

feat(data/two_pointing): Two pointings of a type (#11648) Define `two_pointing α` as the type of two pointings of `α`. This is a Type-valued structure version of `nontrivial`.