Documentation Verification Report

Definability

📁 Source: Mathlib/ModelTheory/Definability.lean

Statistics

Metric	Count
Definitions `DefinableSet`, `instBooleanAlgebra`, `instBot`, `instCompl`, `instHImp`, `instInf`, `instInhabited`, `instPartialOrder`, `instSDiff`, `instSetLike`, `instSup`, `instTop`, `Definable`, `Definable₁`, `Definable₂`, `TermDefinable`, `TermDefinable₁`	17
Theorems `coe_bot`, `coe_compl`, `coe_himp`, `coe_inf`, `coe_sdiff`, `coe_sup`, `coe_top`, `le_iff`, `mem_compl`, `mem_inf`, `mem_sdiff`, `mem_sup`, `mem_top`, `notMem_bot`, `compl`, `himp`, `image_comp`, `image_comp_embedding`, `image_comp_equiv`, `image_comp_sumInl_fin`, `inter`, `map_expansion`, `mono`, `preimage_comp`, `sdiff`, `union`, `comp`, `const`, `definable_tupleGraph`, `map_expansion`, `mono`, `termDefinable₁`, `trans`, `comp`, `comp_termDefinable`, `const`, `definable₂_graph`, `id`, `termDefinable`, `definable_biInter_finset`, `definable_biUnion_finset`, `definable_empty`, `definable_finset_biInter`, `definable_finset_biUnion`, `definable_finset_inf`, `definable_finset_sup`, `definable_iff_empty_definable_with_params`, `definable_iff_exists_formula_sum`, `definable_iff_finitely_definable`, `definable_univ`, `empty_definable_iff`, `termDefinable_empty_iff`, `termDefinable_empty_withConstants_iff`, `termDefinable₁_iff_exists_term`, `termDefinable₁_iff_termDefinable`	55
Total	72

FirstOrder.Language

Definitions

Name	Category	Theorems
`DefinableSet` 📖	CompOp	14 math math: `DefinableSet.mem_top`, `DefinableSet.mem_compl`, `DefinableSet.le_iff`, `DefinableSet.coe_compl`, `DefinableSet.mem_sup`, `DefinableSet.coe_bot`, `DefinableSet.coe_top`, `DefinableSet.coe_sdiff`, `DefinableSet.coe_sup`, `DefinableSet.mem_sdiff`, `DefinableSet.coe_inf`, `DefinableSet.coe_himp`, `DefinableSet.notMem_bot`, `DefinableSet.mem_inf`

FirstOrder.Language.DefinableSet

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	—
`instBot` 📖	CompOp	2 math math: `coe_bot`, `notMem_bot`
`instCompl` 📖	CompOp	2 math math: `mem_compl`, `coe_compl`
`instHImp` 📖	CompOp	1 math math: `coe_himp`
`instInf` 📖	CompOp	2 math math: `coe_inf`, `mem_inf`
`instInhabited` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	1 math math: `le_iff`
`instSDiff` 📖	CompOp	2 math math: `coe_sdiff`, `mem_sdiff`
`instSetLike` 📖	CompOp	14 math math: `mem_top`, `mem_compl`, `le_iff`, `coe_compl`, `mem_sup`, `coe_bot`, `coe_top`, `coe_sdiff`, `coe_sup`, `mem_sdiff`, `coe_inf`, `coe_himp`, `notMem_bot`, `mem_inf`
`instSup` 📖	CompOp	2 math math: `mem_sup`, `coe_sup`
`instTop` 📖	CompOp	2 math math: `mem_top`, `coe_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_compl` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `Compl.compl` `instCompl` `Set` `Set.instCompl`	—	—
`coe_himp` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `HImp.himp` `instHImp` `Set` `BooleanAlgebra.toHImp` `Set.instBooleanAlgebra`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `instInf` `Set` `Set.instInter`	—	—
`coe_sdiff` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `instSDiff` `Set` `Set.instSDiff`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `instSup` `Set` `Set.instUnion`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `FirstOrder.Language.DefinableSet` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`le_iff` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instLE` `SetLike.coe` `instSetLike`	—	—
`mem_compl` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `Compl.compl` `instCompl`	—	—
`mem_inf` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `instInf`	—	—
`mem_sdiff` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `instSDiff`	—	—
`mem_sup` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `instSup`	—	—
`mem_top` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`notMem_bot` 📖	mathematical	—	`FirstOrder.Language.DefinableSet` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot`	—	`Set.notMem_empty`

Set

Definitions

Name	Category	Theorems
`Definable` 📖	MathDef	8 math math: `definable_iff_empty_definable_with_params`, `empty_definable_iff`, `definable_empty`, `definable_iff_exists_formula_sum`, `TermDefinable.definable_tupleGraph`, `FirstOrder.Ring.mvPolynomial_zeroLocus_definable`, `definable_univ`, `definable_iff_finitely_definable`
`Definable₁` 📖	MathDef	—
`Definable₂` 📖	MathDef	1 math math: `TermDefinable₁.definable₂_graph`
`TermDefinable` 📖	MathDef	5 math math: `TermDefinable₁.termDefinable`, `termDefinable_empty_withConstants_iff`, `termDefinable₁_iff_termDefinable`, `TermDefinable.const`, `termDefinable_empty_iff`
`TermDefinable₁` 📖	MathDef	5 math math: `TermDefinable₁.const`, `TermDefinable.termDefinable₁`, `TermDefinable₁.id`, `termDefinable₁_iff_exists_term`, `termDefinable₁_iff_termDefinable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`definable_biInter_finset` 📖	mathematical	`Definable`	`iInter` `Finset` `Finset.instMembership`	—	`Finset.inf_set_eq_iInter` `definable_finset_inf`
`definable_biUnion_finset` 📖	mathematical	`Definable`	`iUnion` `Finset` `Finset.instMembership`	—	`Finset.sup_set_eq_biUnion` `definable_finset_sup`
`definable_empty` 📖	mathematical	—	`Definable` `Set` `instEmptyCollection`	—	`ext`
`definable_finset_biInter` 📖	mathematical	`Definable`	`iInter` `Finset` `Finset.instMembership`	—	`definable_biInter_finset`
`definable_finset_biUnion` 📖	mathematical	`Definable`	`iUnion` `Finset` `Finset.instMembership`	—	`definable_biUnion_finset`
`definable_finset_inf` 📖	mathematical	`Definable`	`Finset.inf` `Set` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `instOrderTop`	—	`Finset.induction` `definable_univ` `Finset.inf_insert` `Definable.inter`
`definable_finset_sup` 📖	mathematical	`Definable`	`Finset.sup` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Finset.induction` `definable_empty` `Finset.sup_insert` `Definable.union`
`definable_iff_empty_definable_with_params` 📖	mathematical	—	`Definable` `Set` `instEmptyCollection` `FirstOrder.Language.withConstants` `Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure`	—	`empty_definable_iff`
`definable_iff_exists_formula_sum` 📖	mathematical	—	`Definable` `setOf` `FirstOrder.Language.Formula.Realize` `Elem` `Set` `instMembership`	—	`Definable.eq_1` `Equiv.exists_congr_left` `ext` `FirstOrder.Language.BoundedFormula.realize_mapTermRel_id` `FirstOrder.Language.isAlgebraic_constantsOn` `Fin.isEmpty'` `FirstOrder.Language.Term.realize_varsToConstants` `FirstOrder.Language.withConstants_expansion` `FirstOrder.Language.Term.realize_relabel`
`definable_iff_finitely_definable` 📖	mathematical	—	`Definable` `Set` `instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.coe_image` `Subtype.coe_preimage_self` `Subtype.coe_eta` `ext` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_restrictFreeVar` `Definable.mono`
`definable_univ` 📖	mathematical	—	`Definable` `univ`	—	`ext`
`empty_definable_iff` 📖	mathematical	—	`Definable` `Set` `instEmptyCollection` `setOf` `FirstOrder.Language.Formula.Realize`	—	`Definable.eq_1` `instIsEmptyElemEmptyCollection` `Equiv.exists_congr_left` `FirstOrder.Language.LHom.setOf_realize_onFormula` `FirstOrder.Language.isAlgebraic_constantsOn` `FirstOrder.Language.isRelational_constantsOn` `FirstOrder.Language.LHom.sumElim_isExpansionOn` `FirstOrder.Language.LHom.id_isExpansionOn` `FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn`
`termDefinable_empty_iff` 📖	mathematical	—	`TermDefinable` `Set` `instEmptyCollection` `FirstOrder.Language.Term.realize`	—	`TermDefinable.eq_1` `instIsEmptyElemEmptyCollection` `Equiv.exists_congr_left` `FirstOrder.Language.isAlgebraic_constantsOn` `FirstOrder.Language.isRelational_constantsOn` `FirstOrder.Language.LHom.realize_onTerm` `FirstOrder.Language.LHom.sumElim_isExpansionOn` `FirstOrder.Language.LHom.id_isExpansionOn` `FirstOrder.Language.LHom.ofIsEmpty_isExpansionOn`
`termDefinable_empty_withConstants_iff` 📖	mathematical	—	`TermDefinable` `Set` `instEmptyCollection` `FirstOrder.Language.withConstants` `Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure`	—	`termDefinable_empty_iff`
`termDefinable₁_iff_exists_term` 📖	mathematical	—	`TermDefinable₁` `FirstOrder.Language.Term.realize` `FirstOrder.Language.withConstants` `Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure`	—	`Equiv.forall_congr'`
`termDefinable₁_iff_termDefinable` 📖	mathematical	—	`TermDefinable₁` `TermDefinable`	—	—

Set.Definable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl` 📖	mathematical	`Set.Definable`	`Compl.compl` `Set` `Set.instCompl`	—	`Set.ext` `Set.compl_setOf` `Set.mem_setOf` `FirstOrder.Language.Formula.realize_not`
`himp` 📖	mathematical	`Set.Definable`	`HImp.himp` `Set` `BooleanAlgebra.toHImp` `Set.instBooleanAlgebra`	—	`himp_eq` `union` `compl`
`image_comp` 📖	mathematical	`Set.Definable`	`Set.image`	—	`nonempty_fintype` `preimage_comp` `image_comp_sumInl_fin` `image_comp_equiv` `Set.ext` `Set.iInter_congr_Prop` `Set.iInter_true` `Set.definable_biInter_finset` `Set.apply_rangeSplitting` `Set.rangeFactorization_coe` `inter`
`image_comp_embedding` 📖	mathematical	`Set.Definable`	`Set.image` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding`	—	`nonempty_fintype` `Function.Embedding.injective` `Set.ext` `image_comp_sumInl_fin` `image_comp_equiv`
`image_comp_equiv` 📖	mathematical	`Set.Definable`	`Set.image` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Set.image_eq_preimage_of_inverse` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `preimage_comp`
`image_comp_sumInl_fin` 📖	mathematical	`Set.Definable`	`Set.image`	—	`Set.ext` `Fin.isEmpty'`
`inter` 📖	mathematical	`Set.Definable`	`Set` `Set.instInter`	—	`Set.ext`
`map_expansion` 📖	—	`Set.Definable`	—	—	`Set.ext` `FirstOrder.Language.addConstants_expansion`
`mono` 📖	—	`Set.Definable` `Set` `Set.instHasSubset`	—	—	`Set.definable_iff_empty_definable_with_params` `map_expansion` `FirstOrder.Language.map_constants_inclusion_isExpansionOn`
`preimage_comp` 📖	mathematical	`Set.Definable`	`Set.preimage`	—	`Set.ext`
`sdiff` 📖	mathematical	`Set.Definable`	`Set` `Set.instSDiff`	—	`inter` `compl`
`union` 📖	mathematical	`Set.Definable`	`Set` `Set.instUnion`	—	`Set.ext` `Set.mem_setOf_eq` `FirstOrder.Language.Formula.realize_sup` `Set.mem_union`

Set.TermDefinable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Set.TermDefinable`	—	—	`FirstOrder.Language.Term.realize_subst`
`const` 📖	mathematical	—	`Set.TermDefinable` `FirstOrder.Language.constantMap` `FirstOrder.Language.withConstants` `Set.Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure`	—	`FirstOrder.Language.Term.realize_constants`
`definable_tupleGraph` 📖	mathematical	`Set.TermDefinable`	`Set.Definable` `Function.tupleGraph`	—	`Set.ext` `FirstOrder.Language.Term.realize_relabel`
`map_expansion` 📖	—	`Set.TermDefinable`	—	—	`FirstOrder.Language.LHom.realize_onTerm` `FirstOrder.Language.addConstants_expansion`
`mono` 📖	—	`Set.TermDefinable` `Set` `Set.instHasSubset`	—	—	`Set.termDefinable_empty_withConstants_iff` `map_expansion` `FirstOrder.Language.map_constants_inclusion_isExpansionOn`
`termDefinable₁` 📖	mathematical	`Set.TermDefinable`	`Set.TermDefinable₁`	—	`Set.termDefinable₁_iff_termDefinable`
`trans` 📖	—	`Set.TermDefinable` `FirstOrder.Language.Term.realize` `FirstOrder.Language.withConstants` `Set.Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure` `FirstOrder.Language.Functions.term`	—	—	`FirstOrder.Language.Term.realize_substFunc`

Set.TermDefinable₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Set.TermDefinable₁`	—	—	`Set.TermDefinable.termDefinable₁` `Set.TermDefinable.comp` `termDefinable`
`comp_termDefinable` 📖	—	`Set.TermDefinable₁` `Set.TermDefinable`	—	—	`Set.TermDefinable.comp` `termDefinable`
`const` 📖	mathematical	—	`Set.TermDefinable₁` `FirstOrder.Language.constantMap` `FirstOrder.Language.withConstants` `Set.Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure`	—	`Set.TermDefinable.termDefinable₁` `Set.TermDefinable.const`
`definable₂_graph` 📖	mathematical	`Set.TermDefinable₁`	`Set.Definable₂` `Function.graph`	—	`Set.TermDefinable.definable_tupleGraph` `termDefinable` `Set.ext` `Set.ext_iff`
`id` 📖	mathematical	—	`Set.TermDefinable₁`	—	—
`termDefinable` 📖	mathematical	`Set.TermDefinable₁`	`Set.TermDefinable`	—	`Set.termDefinable₁_iff_termDefinable`

---

← Back to Index