Commit 2022-07-19 01:02 b36a458a

View on Github →

feat(set_theory/ordinal/basic): add gc_ord_card and gci_ord_card (#15152) Define a Galois coinsertion between cardinal.ord and ordinal.card, then use it to golf some proofs.

Estimated changes

Modified src/order/galois_connection.lean

Modified src/set_theory/ordinal/basic.lean

added theorem cardinal.gc_ord_card

added def cardinal.gci_ord_card

modified theorem cardinal.lt_ord

modified theorem cardinal.lt_ord_succ_card

modified theorem cardinal.ord_card_le

modified theorem cardinal.ord_le_ord

modified theorem cardinal.ord_lt_ord

added theorem cardinal.ord_mono

added theorem cardinal.ord_strict_mono

modified theorem cardinal.ord_zero