Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-08 12:12 91ce04d4

View on Github →

chore(model_theory/encoding): Move the encoding for terms to its own file (#13223) Moves the declarations about encodings and cardinality of terms to their own file, model_theory/encoding

Estimated changes

Created src/model_theory/encoding.lean

added theorem first_order.language.term.card_le

added theorem first_order.language.term.card_le_omega

added def first_order.language.term.list_decode

added theorem first_order.language.term.list_decode_encode_list

added def first_order.language.term.list_encode

added theorem first_order.language.term.list_encode_injective

Modified src/model_theory/substructures.lean

Modified src/model_theory/syntax.lean

deleted theorem first_order.language.term.card_le

deleted theorem first_order.language.term.card_le_omega

deleted def first_order.language.term.list_decode

deleted theorem first_order.language.term.list_decode_encode_list

deleted def first_order.language.term.list_encode

deleted theorem first_order.language.term.list_encode_injective