mathlib3
d3156667 - feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597)

Commit

3 years ago

feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597) Since `cardinal.lift.{(max u v) u} = cardinal.lift.{v u}`, the latter form should be preferred.

Author

vihdzp

Parents

89348848

mathlib3 d3156667 - feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597)

mathlib3
d3156667 - feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597)