Commit 2022-06-08 18:10 d3156667
View on Github →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.
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.