mathlib3
d7ad7d37 - feat(set_theory/cardinal): Upper bound on domain from upper bound on fibers (#13147)

Commit

3 years ago

feat(set_theory/cardinal): Upper bound on domain from upper bound on fibers (#13147) A uniform upper bound on fibers gives an upper bound on the domain.

Author

tb65536

Parents

47a3cd26

mathlib3 d7ad7d37 - feat(set_theory/cardinal): Upper bound on domain from upper bound on fibers (#13147)

mathlib3
d7ad7d37 - feat(set_theory/cardinal): Upper bound on domain from upper bound on fibers (#13147)