Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 14:40 5d8b4328

View on Github →

feat(model_theory/language_map): Cardinality of languages with constants (#13981) first_order.language.card_with_constants shows that the cardinality of L[[A]] is L.card + # A.

Estimated changes

Modified src/logic/equiv/basic.lean

added def equiv.sigma_nat_succ

Modified src/model_theory/basic.lean

added theorem first_order.language.card_mk₂

added theorem first_order.language.constants_mk₂

added theorem first_order.sequence₂.lift_mk

added theorem first_order.sequence₂.sum_card

modified def first_order.sequence₂

Modified src/model_theory/bundled.lean

Modified src/model_theory/language_map.lean

added theorem first_order.language.card_constants_on

added theorem first_order.language.card_with_constants

modified def first_order.language.constants_on

modified theorem first_order.language.constants_on_constants

deleted def first_order.language.constants_on_functions

Modified src/model_theory/substructures.lean

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.sum_nat_eq_add_sum_succ