Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-25 10:04 6b322417

View on Github →

feat(model_theory/basic): Terms, formulas, and definable sets (#11067) Defines first-order terms, formulas, sentences and theories Defines the boolean algebra of definable sets (Several of these definitions are based on those from the flypitch project.)

Estimated changes

Modified src/model_theory/basic.lean

added def first_order.language.bd_not

added inductive first_order.language.bounded_formula

added theorem first_order.language.definable_set.coe_bot

added theorem first_order.language.definable_set.coe_compl

added theorem first_order.language.definable_set.coe_inf

added theorem first_order.language.definable_set.coe_sup

added theorem first_order.language.definable_set.coe_top

added theorem first_order.language.definable_set.le_iff

added theorem first_order.language.definable_set.mem_compl

added theorem first_order.language.definable_set.mem_inf

added theorem first_order.language.definable_set.mem_sup

added theorem first_order.language.definable_set.mem_top

added theorem first_order.language.definable_set.not_mem_bot

added def first_order.language.definable_set

added def first_order.language.formula

added theorem first_order.language.is_definable.compl

added theorem first_order.language.is_definable.inter

added theorem first_order.language.is_definable.sdiff

added theorem first_order.language.is_definable.union

added structure first_order.language.is_definable

added theorem first_order.language.is_definable_empty

added theorem first_order.language.is_definable_univ

added def first_order.language.realize_bounded_formula

added def first_order.language.realize_formula

added theorem first_order.language.realize_not

added def first_order.language.realize_sentence

added def first_order.language.realize_term

added def first_order.language.sentence

added inductive first_order.language.term

added def first_order.language.theory