mathlib

d831478d - feat(computability/encoding): Bounds on cardinality from an encoding (#13224)

feat(computability/encoding): Bounds on cardinality from an encoding (#13224) Generalizes universe variables for `computability.encoding` Uses a `computability.encoding` to bound the cardinality of a type