Semantics

📁 Source: Mathlib/ModelTheory/Semantics.lean

Statistics

Metric	Count
Definitions `Realize`, `ElementarilyEquivalent`, `Realize`, `Realize`, `realize`, `Model`, `completeTheory`, `«term_⊨__1»`, `«term_⊨_»`, `«term_≅[_]_»`	10
Theorems `realize_all`, `realize_all_liftAt_one_self`, `realize_alls`, `realize_bdEqual`, `realize_bot`, `realize_castLE_of_eq`, `realize_constantsVarsEquiv`, `realize_ex`, `realize_exs`, `realize_foldr_imp`, `realize_foldr_inf`, `realize_foldr_sup`, `realize_iAlls`, `realize_iExs`, `realize_iExsUnique`, `realize_iInf`, `realize_iSup`, `realize_iff`, `realize_imp`, `realize_inf`, `realize_liftAt`, `realize_liftAt_one`, `realize_liftAt_one_self`, `realize_mapTermRel_add_castLe`, `realize_mapTermRel_id`, `realize_not`, `realize_rel`, `realize_relabel`, `realize_relabelEquiv`, `realize_rel₁`, `realize_rel₂`, `realize_restrictFreeVar`, `realize_restrictFreeVar'`, `realize_subst`, `realize_sup`, `realize_toFormula`, `realize_top`, `completeTheory_eq`, `infinite`, `infinite_iff`, `nonempty`, `nonempty_iff`, `realize_sentence`, `theory_model`, `theory_model_iff`, `trans`, `boundedFormula_realize_eq_realize`, `realize_bot`, `realize_equal`, `realize_equivSentence`, `realize_equivSentence_symm`, `realize_equivSentence_symm_con`, `realize_graph`, `realize_iAlls`, `realize_iExs`, `realize_iExsUnique`, `realize_iInf`, `realize_iSup`, `realize_iff`, `realize_imp`, `realize_inf`, `realize_not`, `realize_rel`, `realize_relabel`, `realize_relabel_sumInr`, `realize_rel₁`, `realize_rel₂`, `realize_sup`, `realize_top`, `realize_term`, `onTheory_model`, `realize_onBoundedFormula`, `realize_onFormula`, `realize_onSentence`, `realize_onTerm`, `setOf_realize_onFormula`, `realize_antisymmetric`, `realize_irreflexive`, `realize_reflexive`, `realize_symmetric`, `realize_total`, `realize_transitive`, `realize_cardGe`, `realize_not`, `elementarilyEquivalent`, `realize_boundedFormula`, `realize_formula`, `realize_sentence`, `theory_model`, `realize_con`, `realize_constants`, `realize_constantsToVars`, `realize_constantsVarsEquivLeft`, `realize_func`, `realize_function_term`, `realize_functions_apply₁`, `realize_functions_apply₂`, `realize_liftAt`, `realize_relabel`, `realize_restrictVar`, `realize_restrictVar'`, `realize_restrictVarLeft`, `realize_restrictVarLeft'`, `realize_subst`, `realize_substFunc`, `realize_var`, `realize_varsToConstants`, `mono`, `realize_of_mem`, `union`, `subset`, `model_iff`, `model_iff_subset_completeTheory`, `model_insert_iff`, `model_singleton_iff`, `model_union_iff`, `realize_sentence_of_mem`, `card_le_of_model_distinctConstantsTheory`, `elementarilyEquivalent_iff`, `mem_completeTheory`, `model_completeTheory`, `model_distinctConstantsTheory`, `model_empty`, `model_infiniteTheory`, `model_infiniteTheory_iff`, `model_nonempty`, `model_nonemptyTheory_iff`, `realize_iff_of_model_completeTheory`	128
Total	138

FirstOrder

Definitions

Name	Category	Theorems
`«term_≅[_]_»` 📖	CompOp	—

FirstOrder.Language

Definitions

Name	Category	Theorems
`ElementarilyEquivalent` 📖	MathDef	7 math math: `exists_elementarilyEquivalent_card_eq`, `ElementaryEmbedding.elementarilyEquivalent`, `elementarilyEquivalent_iff`, `Theory.IsComplete.models_elementarily_equivalent`, `ElementarySubstructure.elementarilyEquivalent`, `Theory.IsComplete.isComplete_iff_models_elementarily_equivalent`, `StrongHomClass.elementarilyEquivalent`
`completeTheory` 📖	CompOp	10 math math: `ElementarilyEquivalent.completeTheory_eq`, `completeTheory.isMaximal`, `Theory.model_iff_subset_completeTheory`, `mem_completeTheory`, `completeTheory.mem_or_not_mem`, `Theory.IsComplete.eq_complete_theory`, `completeTheory.isSatisfiable`, `completeTheory.isComplete`, `Theory.completeTheory.subset`, `model_completeTheory`
`«term_⊨__1»` 📖	CompOp	—
`«term_⊨_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_of_model_distinctConstantsTheory` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `Set.Elem`	—	`Cardinal.lift_mk_le'` `Set.injOn_iff_injective` `model_distinctConstantsTheory`
`elementarilyEquivalent_iff` 📖	mathematical	—	`ElementarilyEquivalent` `Sentence.Realize`	—	—
`mem_completeTheory` 📖	mathematical	—	`Sentence` `Theory` `Set.instMembership` `completeTheory` `Sentence.Realize`	—	—
`model_completeTheory` 📖	mathematical	—	`Theory.Model` `completeTheory`	—	`Theory.model_iff_subset_completeTheory` `subset_rfl` `Set.instReflSubset`
`model_distinctConstantsTheory` 📖	mathematical	—	`Theory.Model` `withConstants` `distinctConstantsTheory` `Set.InjOn` `constantMap` `con`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Empty.instIsEmpty` `Term.realize_constants`
`model_empty` 📖	mathematical	—	`Theory.Model` `Theory` `Set.instEmptyCollection` `Sentence`	—	`Set.notMem_empty`
`model_infiniteTheory` 📖	mathematical	—	`Theory.Model` `infiniteTheory`	—	`model_infiniteTheory_iff`
`model_infiniteTheory_iff` 📖	mathematical	—	`Theory.Model` `infiniteTheory` `Infinite`	—	—
`model_nonempty` 📖	mathematical	—	`Theory.Model` `nonemptyTheory`	—	`model_nonemptyTheory_iff`
`model_nonemptyTheory_iff` 📖	mathematical	—	`Theory.Model` `nonemptyTheory`	—	`Nat.cast_one`
`realize_iff_of_model_completeTheory` 📖	mathematical	—	`Sentence.Realize`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Sentence.realize_not` `Theory.realize_sentence_of_mem` `mem_completeTheory`

FirstOrder.Language.BoundedFormula

Definitions

Name	Category	Theorems
`Realize` 📖	MathDef	52 math math: `FirstOrder.Language.LHom.realize_onBoundedFormula`, `realize_foldr_imp`, `realize_inf`, `realize_ex`, `realize_iExsUnique`, `realize_toPrenexImp`, `realize_iExs`, `realize_iSup`, `realize_not`, `realize_all`, `realize_foldr_sup`, `FirstOrder.Language.ElementaryEmbedding.map_boundedFormula`, `FirstOrder.Language.Formula.realize_relabel_sumInr`, `realize_liftAt_one`, `realize_relabel`, `realize_subst`, `realize_rel₁`, `FirstOrder.Language.Term.realize_le`, `FirstOrder.Language.Term.realize_lt`, `realize_relabelEquiv`, `realize_toPrenex`, `realize_bot`, `realize_iAlls`, `realize_restrictFreeVar'`, `IsQF.realize_embedding`, `realize_foldr_inf`, `realize_liftAt_one_self`, `realize_exs`, `realize_all_liftAt_one_self`, `realize_top`, `FirstOrder.Language.Ultraproduct.boundedFormula_realize_cast`, `realize_rel`, `realize_iff`, `realize_bdEqual`, `realize_alls`, `realize_constantsVarsEquiv`, `FirstOrder.Language.StrongHomClass.realize_boundedFormula`, `realize_iInf`, `realize_toPrenexImpRight`, `FirstOrder.Language.Substructure.realize_boundedFormula_top`, `realize_imp`, `realize_mapTermRel_add_castLe`, `realize_mapTermRel_id`, `realize_liftAt`, `realize_sup`, `FirstOrder.Language.Theory.Iff.realize_bd_iff`, `FirstOrder.Language.Formula.boundedFormula_realize_eq_realize`, `realize_toFormula`, `realize_restrictFreeVar`, `realize_castLE_of_eq`, `FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula`, `realize_rel₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_all` 📖	mathematical	—	`Realize` `all` `Fin.snoc`	—	—
`realize_all_liftAt_one_self` 📖	mathematical	—	`Realize` `all` `liftAt`	—	`Fin.snoc_comp_castSucc`
`realize_alls` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `alls` `Realize`	—	`Fin.isEmpty'` `Unique.forall_iff` `Fin.snoc_init_self`
`realize_bdEqual` 📖	mathematical	—	`Realize` `FirstOrder.Language.Term.bdEqual` `FirstOrder.Language.Term.realize`	—	—
`realize_bot` 📖	mathematical	—	`Realize` `Bot.bot` `FirstOrder.Language.BoundedFormula` `instBot`	—	—
`realize_castLE_of_eq` 📖	mathematical	—	`Realize` `castLE`	—	`castLE_rfl`
`realize_constantsVarsEquiv` 📖	mathematical	—	`Realize` `DFunLike.coe` `Equiv` `FirstOrder.Language.BoundedFormula` `FirstOrder.Language.withConstants` `EquivLike.toFunLike` `Equiv.instEquivLike` `constantsVarsEquiv` `FirstOrder.Language.constantMap` `FirstOrder.Language.con`	—	`realize_mapTermRel_id` `FirstOrder.Language.isAlgebraic_constantsOn` `FirstOrder.Language.Term.realize_constantsVarsEquivLeft` `FirstOrder.Language.LHom.map_onRelation`
`realize_ex` 📖	mathematical	—	`Realize` `ex` `Fin.snoc`	—	`ex.eq_1` `realize_not` `realize_all`
`realize_exs` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `exs` `Realize`	—	`Fin.isEmpty'` `Unique.exists_iff` `Fin.snoc_init_self`
`realize_foldr_imp` 📖	mathematical	—	`Realize` `FirstOrder.Language.BoundedFormula` `imp`	—	`instIsEmptyFalse`
`realize_foldr_inf` 📖	mathematical	—	`Realize` `FirstOrder.Language.BoundedFormula` `instMin` `Top.top` `instTop`	—	`instIsEmptyFalse`
`realize_foldr_sup` 📖	mathematical	—	`Realize` `FirstOrder.Language.BoundedFormula` `instMax` `Bot.bot` `instBot`	—	—
`realize_iAlls` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula.iAlls` `FirstOrder.Language.Formula.Realize`	—	`FirstOrder.Language.Formula.realize_iAlls` `Fin.isEmpty'` `Unique.instSubsingleton`
`realize_iExs` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula.iExs` `FirstOrder.Language.Formula.Realize`	—	`FirstOrder.Language.Formula.realize_iExs` `Fin.isEmpty'` `Unique.instSubsingleton`
`realize_iExsUnique` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula.iExsUnique` `ExistsUnique` `FirstOrder.Language.Formula.Realize`	—	`FirstOrder.Language.Formula.realize_iExsUnique` `Fin.isEmpty'` `Unique.instSubsingleton`
`realize_iInf` 📖	mathematical	—	`Realize` `iInf`	—	—
`realize_iSup` 📖	mathematical	—	`Realize` `iSup`	—	—
`realize_iff` 📖	mathematical	—	`Realize` `iff`	—	—
`realize_imp` 📖	mathematical	—	`Realize` `imp`	—	—
`realize_inf` 📖	mathematical	—	`Realize` `FirstOrder.Language.BoundedFormula` `instMin`	—	—
`realize_liftAt` 📖	mathematical	—	`Realize` `liftAt`	—	`liftAt.eq_1` `FirstOrder.Language.Term.realize_liftAt` `add_assoc` `add_comm` `realize_castLE_of_eq` `LE.le.trans` `iff_eq_eq` `Fin.snoc_last` `Fin.snoc_castSucc`
`realize_liftAt_one` 📖	mathematical	—	`Realize` `liftAt`	—	`covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le`
`realize_liftAt_one_self` 📖	mathematical	—	`Realize` `liftAt`	—	`realize_liftAt_one` `refl` `instReflLe` `iff_eq_eq`
`realize_mapTermRel_add_castLe` 📖	mathematical	`FirstOrder.Language.Term.realize` `FirstOrder.Language.Structure.RelMap` `Fin.snoc`	`Realize` `mapTermRel` `castLE` `Eq.le` `Nat.instPreorder` `AddSemigroup.toAdd` `Nat.instAddSemigroup` `add_assoc`	—	`Eq.le` `add_assoc` `castLE_rfl` `Fin.snoc_comp_natAdd`
`realize_mapTermRel_id` 📖	mathematical	`FirstOrder.Language.Term.realize` `FirstOrder.Language.Structure.RelMap`	`Realize` `mapTermRel` `FirstOrder.Language.BoundedFormula`	—	—
`realize_not` 📖	mathematical	—	`Realize` `not`	—	—
`realize_rel` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.boundedFormula` `FirstOrder.Language.Structure.RelMap` `FirstOrder.Language.Term.realize`	—	—
`realize_relabel` 📖	mathematical	—	`Realize` `relabel`	—	`realize_mapTermRel_add_castLe` `FirstOrder.Language.Term.realize_relabel` `sumElim_comp_relabelAux` `Fin.snoc_comp_castAdd`
`realize_relabelEquiv` 📖	mathematical	—	`Realize` `DFunLike.coe` `Equiv` `FirstOrder.Language.BoundedFormula` `EquivLike.toFunLike` `Equiv.instEquivLike` `relabelEquiv`	—	`realize_mapTermRel_id` `FirstOrder.Language.Term.realize_relabel`
`realize_rel₁` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.boundedFormula₁` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `FirstOrder.Language.Term.realize` `Matrix.vecEmpty`	—	`FirstOrder.Language.Relations.boundedFormula₁.eq_1` `realize_rel` `iff_eq_eq` `Matrix.cons_val_fin_one`
`realize_rel₂` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.boundedFormula₂` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `FirstOrder.Language.Term.realize` `Matrix.vecEmpty`	—	`FirstOrder.Language.Relations.boundedFormula₂.eq_1` `realize_rel` `iff_eq_eq` `Matrix.cons_val_succ` `Matrix.cons_val_fin_one`
`realize_restrictFreeVar` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `freeVarFinset`	`Realize` `restrictFreeVar`	—	`FirstOrder.Language.Term.realize_restrictVarLeft`
`realize_restrictFreeVar'` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `freeVarFinset`	`Realize` `Set.Elem` `restrictFreeVar` `Set.inclusion` `Set.instMembership`	—	`realize_restrictFreeVar`
`realize_subst` 📖	mathematical	—	`Realize` `subst` `FirstOrder.Language.Term.realize`	—	`realize_mapTermRel_id` `FirstOrder.Language.Term.realize_subst` `FirstOrder.Language.Term.realize_relabel`
`realize_sup` 📖	mathematical	—	`Realize` `FirstOrder.Language.BoundedFormula` `instMax`	—	—
`realize_toFormula` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `toFormula` `Realize`	—	`toFormula.eq_4` `Fin.isEmpty'` `FirstOrder.Language.Formula.Realize.eq_1` `realize_imp` `toFormula.eq_5` `realize_all` `realize_relabel` `finSumFinEquiv_symm_last` `finSumFinEquiv_symm_apply_castAdd` `Fin.snoc_castSucc`
`realize_top` 📖	mathematical	—	`Realize` `Top.top` `FirstOrder.Language.BoundedFormula` `instTop`	—	—

FirstOrder.Language.ElementarilyEquivalent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeTheory_eq` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`FirstOrder.Language.completeTheory`	—	—
`infinite` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`Infinite`	—	`infinite_iff`
`infinite_iff` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`Infinite`	—	`FirstOrder.Language.model_infiniteTheory_iff` `theory_model_iff`
`nonempty` 📖	—	`FirstOrder.Language.ElementarilyEquivalent`	—	—	`nonempty_iff`
`nonempty_iff` 📖	—	`FirstOrder.Language.ElementarilyEquivalent`	—	—	`FirstOrder.Language.model_nonemptyTheory_iff` `theory_model_iff`
`realize_sentence` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`FirstOrder.Language.Sentence.Realize`	—	`FirstOrder.Language.elementarilyEquivalent_iff`
`theory_model` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`FirstOrder.Language.Theory.Model`	—	`theory_model_iff`
`theory_model_iff` 📖	mathematical	`FirstOrder.Language.ElementarilyEquivalent`	`FirstOrder.Language.Theory.Model`	—	`FirstOrder.Language.Theory.model_iff_subset_completeTheory` `completeTheory_eq`
`trans` 📖	—	`FirstOrder.Language.ElementarilyEquivalent`	—	—	—

FirstOrder.Language.Formula

Definitions

Name	Category	Theorems
`Realize` 📖	MathDef	46 math math: `realize_bot`, `FirstOrder.Language.LHom.setOf_realize_onFormula`, `realize_rel`, `realize_rel₁`, `Set.empty_definable_iff`, `realize_equal`, `FirstOrder.Field.realize_eqZero`, `FirstOrder.Language.BoundedFormula.realize_iExsUnique`, `Set.definable_iff_exists_formula_sum`, `realize_iff`, `FirstOrder.Language.Theory.models_formula_iff`, `realize_rel₂`, `FirstOrder.Language.LHom.realize_onFormula`, `FirstOrder.Language.BoundedFormula.realize_iExs`, `FirstOrder.Language.Ultraproduct.realize_formula_cast`, `FirstOrder.Language.Substructure.realize_formula_top`, `realize_iAlls`, `realize_relabel_sumInr`, `realize_relabel`, `realize_iSup`, `FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula`, `FirstOrder.Language.BoundedFormula.realize_iAlls`, `realize_equivSentence_symm_con`, `FirstOrder.Language.Theory.Iff.realize_iff`, `FirstOrder.Language.StrongHomClass.realize_formula`, `realize_graph`, `FirstOrder.Language.BoundedFormula.realize_exs`, `FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf`, `realize_iInf`, `FirstOrder.realize_genericPolyMapSurjOnOfInjOn`, `realize_not`, `FirstOrder.Language.BoundedFormula.realize_alls`, `realize_sup`, `FirstOrder.Language.Theory.CompleteType.mem_typeOf`, `realize_inf`, `realize_iExsUnique`, `realize_imp`, `realize_top`, `FirstOrder.Language.Embedding.isElementary_of_exists`, `FirstOrder.Language.ElementaryEmbedding.map_formula`, `FirstOrder.Language.ElementaryEmbedding.map_formula'`, `boundedFormula_realize_eq_realize`, `realize_iExs`, `FirstOrder.Language.BoundedFormula.realize_toFormula`, `realize_equivSentence_symm`, `realize_equivSentence`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boundedFormula_realize_eq_realize` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `Realize`	—	`Fin.isEmpty'` `Realize.eq_1`
`realize_bot` 📖	mathematical	—	`Realize` `Bot.bot` `FirstOrder.Language.Formula` `FirstOrder.Language.BoundedFormula.instBot`	—	—
`realize_equal` 📖	mathematical	—	`Realize` `FirstOrder.Language.Term.equal` `FirstOrder.Language.Term.realize`	—	`Fin.isEmpty'` `FirstOrder.Language.Term.realize_relabel`
`realize_equivSentence` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `FirstOrder.Language.withConstants` `DFunLike.coe` `Equiv` `FirstOrder.Language.Formula` `FirstOrder.Language.Sentence` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivSentence` `Realize` `FirstOrder.Language.constantMap` `FirstOrder.Language.con`	—	`realize_equivSentence_symm_con` `Equiv.symm_apply_apply`
`realize_equivSentence_symm` 📖	mathematical	—	`Realize` `DFunLike.coe` `Equiv` `FirstOrder.Language.Sentence` `FirstOrder.Language.withConstants` `FirstOrder.Language.Formula` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSentence` `FirstOrder.Language.Sentence.Realize` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.constantsOn.structure`	—	`realize_equivSentence_symm_con` `FirstOrder.Language.withConstants_expansion`
`realize_equivSentence_symm_con` 📖	mathematical	—	`Realize` `DFunLike.coe` `Equiv` `FirstOrder.Language.Sentence` `FirstOrder.Language.withConstants` `FirstOrder.Language.Formula` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivSentence` `FirstOrder.Language.constantMap` `FirstOrder.Language.con` `FirstOrder.Language.Sentence.Realize`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `iff_isEquiv` `FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv`
`realize_graph` 📖	mathematical	—	`Realize` `graph` `Fin.cons` `FirstOrder.Language.Structure.funMap`	—	`Fin.cons_zero` `Fin.cons_succ`
`realize_iAlls` 📖	mathematical	—	`Realize` `iAlls`	—	`Finite.exists_equiv_fin` `iAlls.eq_1` `Equiv.forall_congr` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `Fin.isEmpty'` `Realize.eq_1`
`realize_iExs` 📖	mathematical	—	`Realize` `iExs`	—	`Finite.exists_equiv_fin` `iExs.eq_1` `Equiv.exists_congr` `Equiv.apply_symm_apply` `Equiv.symm_apply_apply` `Fin.isEmpty'` `Realize.eq_1`
`realize_iExsUnique` 📖	mathematical	—	`Realize` `iExsUnique` `ExistsUnique`	—	`iExsUnique.eq_1` `ExistsUnique.eq_1` `Fin.isEmpty'`
`realize_iInf` 📖	mathematical	—	`Realize` `iInf`	—	`Fin.isEmpty'`
`realize_iSup` 📖	mathematical	—	`Realize` `iSup`	—	`Fin.isEmpty'`
`realize_iff` 📖	mathematical	—	`Realize` `iff`	—	`FirstOrder.Language.BoundedFormula.realize_iff` `Fin.isEmpty'`
`realize_imp` 📖	mathematical	—	`Realize` `imp`	—	`FirstOrder.Language.BoundedFormula.realize_imp` `Fin.isEmpty'`
`realize_inf` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula` `FirstOrder.Language.BoundedFormula.instMin`	—	`FirstOrder.Language.BoundedFormula.realize_inf` `Fin.isEmpty'`
`realize_not` 📖	mathematical	—	`Realize` `not`	—	—
`realize_rel` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.formula` `FirstOrder.Language.Structure.RelMap` `FirstOrder.Language.Term.realize`	—	`Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel` `FirstOrder.Language.Term.realize_relabel`
`realize_relabel` 📖	mathematical	—	`Realize` `relabel`	—	`Fin.isEmpty'` `Realize.eq_1` `relabel.eq_1` `FirstOrder.Language.BoundedFormula.realize_relabel` `iff_eq_eq`
`realize_relabel_sumInr` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `FirstOrder.Language.BoundedFormula.relabel` `Realize`	—	`FirstOrder.Language.BoundedFormula.realize_relabel` `Fin.isEmpty'` `Realize.eq_1` `Unique.instSubsingleton`
`realize_rel₁` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.formula₁` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `FirstOrder.Language.Term.realize` `Matrix.vecEmpty`	—	`FirstOrder.Language.Relations.formula₁.eq_1` `realize_rel` `iff_eq_eq` `Matrix.cons_val_fin_one`
`realize_rel₂` 📖	mathematical	—	`Realize` `FirstOrder.Language.Relations.formula₂` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `FirstOrder.Language.Term.realize` `Matrix.vecEmpty`	—	`FirstOrder.Language.Relations.formula₂.eq_1` `realize_rel` `iff_eq_eq` `Matrix.cons_val_succ` `Matrix.cons_val_fin_one`
`realize_sup` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula` `FirstOrder.Language.BoundedFormula.instMax`	—	`FirstOrder.Language.BoundedFormula.realize_sup` `Fin.isEmpty'`
`realize_top` 📖	mathematical	—	`Realize` `Top.top` `FirstOrder.Language.Formula` `FirstOrder.Language.BoundedFormula.instTop`	—	`FirstOrder.Language.BoundedFormula.realize_top` `Fin.isEmpty'`

FirstOrder.Language.HomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_term` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `DFunLike.coe`	—	`FirstOrder.Language.Term.realize.eq_2` `map_fun`

FirstOrder.Language.LHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`onTheory_model` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `onTheory`	—	—
`realize_onBoundedFormula` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `onBoundedFormula`	—	`realize_onTerm` `map_onRelation`
`realize_onFormula` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `onFormula`	—	`realize_onBoundedFormula` `Fin.isEmpty'`
`realize_onSentence` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `onSentence`	—	`realize_onFormula` `Empty.instIsEmpty`
`realize_onTerm` 📖	mathematical	—	`FirstOrder.Language.Term.realize` `onTerm`	—	`map_onFunction`
`setOf_realize_onFormula` 📖	mathematical	—	`setOf` `FirstOrder.Language.Formula.Realize` `onFormula`	—	`Set.ext`

FirstOrder.Language.Relations

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_antisymmetric` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `antisymmetric` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel₂`
`realize_irreflexive` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `irreflexive` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel₂`
`realize_reflexive` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `reflexive` `Reflexive` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel₂`
`realize_symmetric` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `symmetric` `Symmetric` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel₂`
`realize_total` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `total` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_sup` `FirstOrder.Language.BoundedFormula.realize_rel₂`
`realize_transitive` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize` `transitive` `Transitive` `FirstOrder.Language.Structure.RelMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Empty.instIsEmpty` `Fin.isEmpty'` `FirstOrder.Language.BoundedFormula.realize_rel₂`

FirstOrder.Language.Sentence

Definitions

Name	Category	Theorems
`Realize` 📖	MathDef	38 math math: `FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence`, `FirstOrder.Field.realize_genericMonicPolyHasRoot`, `FirstOrder.Language.realize_denselyOrdered_iff`, `FirstOrder.Language.realize_noTopOrder_iff`, `FirstOrder.Language.Relations.realize_irreflexive`, `FirstOrder.Language.StrongHomClass.realize_sentence`, `realize_cardGe`, `FirstOrder.Language.ElementaryEmbedding.map_sentence`, `FirstOrder.Language.realize_noBotOrder_iff`, `FirstOrder.Language.Theory.model_iff`, `FirstOrder.Language.elementarilyEquivalent_iff`, `realize_not`, `FirstOrder.Language.Theory.Iff.models_sentence_iff`, `FirstOrder.Language.Relations.realize_transitive`, `FirstOrder.Language.Theory.Model.realize_of_mem`, `FirstOrder.Language.realize_iff_of_model_completeTheory`, `FirstOrder.Language.realize_noBotOrder`, `FirstOrder.Language.realize_noTopOrder`, `FirstOrder.Language.Theory.model_singleton_iff`, `FirstOrder.Language.Theory.models_sentence_iff`, `FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp`, `FirstOrder.Language.Ultraproduct.sentence_realize`, `FirstOrder.Language.Relations.realize_total`, `FirstOrder.Language.Formula.realize_equivSentence_symm_con`, `FirstOrder.Language.Theory.model_insert_iff`, `FirstOrder.Language.mem_completeTheory`, `FirstOrder.Language.Relations.realize_symmetric`, `FirstOrder.realize_genericPolyMapSurjOnOfInjOn`, `FirstOrder.Language.ElementarySubstructure.realize_sentence`, `FirstOrder.Language.Theory.IsComplete.realize_sentence_iff`, `FirstOrder.Language.LHom.realize_onSentence`, `FirstOrder.Language.realize_denselyOrdered`, `FirstOrder.Language.Theory.realize_sentence_of_mem`, `FirstOrder.Language.Relations.realize_reflexive`, `FirstOrder.Language.ElementarilyEquivalent.realize_sentence`, `FirstOrder.Language.Formula.realize_equivSentence_symm`, `FirstOrder.Language.Formula.realize_equivSentence`, `FirstOrder.Language.Relations.realize_antisymmetric`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_cardGe` 📖	mathematical	—	`Realize` `cardGe` `Cardinal` `Cardinal.instLE` `Cardinal.instNatCast`	—	`Cardinal.lift_mk_fin` `Cardinal.lift_le` `Cardinal.lift_lift` `Cardinal.lift_mk_le` `cardGe.eq_1` `Empty.instIsEmpty` `Realize.eq_1` `FirstOrder.Language.BoundedFormula.realize_exs` `Mathlib.Tactic.Contrapose.contrapose₁` `Function.instEmbeddingLikeEmbedding`
`realize_not` 📖	mathematical	—	`Realize` `FirstOrder.Language.Formula.not`	—	—

FirstOrder.Language.StrongHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elementarilyEquivalent` 📖	mathematical	—	`FirstOrder.Language.ElementarilyEquivalent`	—	`FirstOrder.Language.elementarilyEquivalent_iff` `realize_sentence`
`realize_boundedFormula` 📖	mathematical	—	`FirstOrder.Language.BoundedFormula.Realize` `DFunLike.coe` `EquivLike.toFunLike`	—	`FirstOrder.Language.HomClass.realize_term` `homClass` `EmbeddingLike.apply_eq_iff_eq` `EquivLike.toEmbeddingLike` `map_rel` `FirstOrder.Language.BoundedFormula.Realize.eq_4` `FirstOrder.Language.BoundedFormula.Realize.eq_5` `Fin.comp_snoc` `EquivLike.apply_inv_apply`
`realize_formula` 📖	mathematical	—	`FirstOrder.Language.Formula.Realize` `DFunLike.coe` `EquivLike.toFunLike`	—	`Fin.isEmpty'` `FirstOrder.Language.Formula.Realize.eq_1` `realize_boundedFormula` `iff_eq_eq` `Unique.eq_default`
`realize_sentence` 📖	mathematical	—	`FirstOrder.Language.Sentence.Realize`	—	`Empty.instIsEmpty` `FirstOrder.Language.Sentence.Realize.eq_1` `realize_formula` `Unique.eq_default`
`theory_model` 📖	mathematical	—	`FirstOrder.Language.Theory.Model`	—	`realize_sentence` `FirstOrder.Language.Theory.realize_sentence_of_mem`

FirstOrder.Language.Term

Definitions

Name	Category	Theorems
`realize` 📖	CompOp	50 math math: `FirstOrder.Ring.realize_neg`, `FirstOrder.Language.Formula.realize_rel`, `FirstOrder.Language.Formula.realize_rel₁`, `FirstOrder.Language.Formula.realize_equal`, `realize_function_term`, `realize_liftAt`, `FirstOrder.Ring.realize_termOfFreeCommRing`, `FirstOrder.Language.Formula.realize_rel₂`, `FirstOrder.Language.presburger.realize_sum`, `FirstOrder.Language.presburger.realize_add`, `realize_restrictVar`, `FirstOrder.Language.Substructure.mem_closure_iff_exists_term`, `realize_restrictVarLeft'`, `FirstOrder.Language.presburger.realize_natCast`, `realize_constantsToVars`, `FirstOrder.Language.realize_term_substructure`, `realize_relabel`, `realize_subst`, `FirstOrder.Language.BoundedFormula.realize_subst`, `FirstOrder.Language.presburger.realize_one`, `FirstOrder.Language.BoundedFormula.realize_rel₁`, `FirstOrder.Language.presburger.realize_zero`, `FirstOrder.Ring.realize_add`, `realize_le`, `realize_lt`, `realize_constants`, `realize_constantsVarsEquivLeft`, `Set.termDefinable₁_iff_exists_term`, `FirstOrder.Language.HomClass.realize_term`, `realize_var`, `realize_con`, `realize_quotient_mk'`, `FirstOrder.Ring.realize_mul`, `FirstOrder.Language.presburger.realize_nsmul`, `FirstOrder.Ring.realize_zero`, `FirstOrder.Ring.realize_one`, `FirstOrder.Language.LHom.realize_onTerm`, `FirstOrder.Language.BoundedFormula.realize_rel`, `FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize`, `FirstOrder.Language.BoundedFormula.realize_bdEqual`, `FirstOrder.Language.Ultraproduct.term_realize_cast`, `realize_func`, `realize_restrictVarLeft`, `realize_varsToConstants`, `Set.termDefinable_empty_iff`, `realize_mem`, `realize_functions_apply₂`, `realize_restrictVar'`, `FirstOrder.Language.BoundedFormula.realize_rel₂`, `realize_functions_apply₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`realize_con` 📖	mathematical	—	`realize` `FirstOrder.Language.withConstants` `Set.Elem` `FirstOrder.Language.withConstantsStructure` `FirstOrder.Language.paramsStructure` `FirstOrder.Language.Constants.term` `FirstOrder.Language.con` `Set` `Set.instMembership`	—	—
`realize_constants` 📖	mathematical	—	`realize` `FirstOrder.Language.Constants.term` `FirstOrder.Language.constantMap`	—	`FirstOrder.Language.funMap_eq_coe_constants` `Fin.isEmpty'`
`realize_constantsToVars` 📖	mathematical	—	`realize` `FirstOrder.Language.constantMap` `FirstOrder.Language.withConstants` `FirstOrder.Language.con` `constantsToVars`	—	`FirstOrder.Language.withConstants_funMap_sumInl` `FirstOrder.Language.funMap_eq_coe_constants` `FirstOrder.Language.isEmpty_functions_constantsOn_succ`
`realize_constantsVarsEquivLeft` 📖	mathematical	—	`realize` `FirstOrder.Language.constantMap` `FirstOrder.Language.withConstants` `FirstOrder.Language.con` `DFunLike.coe` `Equiv` `FirstOrder.Language.Term` `EquivLike.toFunLike` `Equiv.instEquivLike` `constantsVarsEquivLeft`	—	`realize_relabel` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `realize_constantsToVars`
`realize_func` 📖	mathematical	—	`realize` `func` `FirstOrder.Language.Structure.funMap`	—	—
`realize_function_term` 📖	mathematical	—	`realize` `FirstOrder.Language.Functions.term` `FirstOrder.Language.Structure.funMap`	—	—
`realize_functions_apply₁` 📖	mathematical	—	`realize` `FirstOrder.Language.Functions.apply₁` `FirstOrder.Language.Structure.funMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`FirstOrder.Language.Functions.apply₁.eq_1` `realize.eq_2` `Matrix.cons_val_fin_one`
`realize_functions_apply₂` 📖	mathematical	—	`realize` `FirstOrder.Language.Functions.apply₂` `FirstOrder.Language.Structure.funMap` `Matrix.vecCons` `Matrix.vecEmpty`	—	`FirstOrder.Language.Functions.apply₂.eq_1` `realize.eq_2` `Matrix.cons_val_succ` `Matrix.cons_val_fin_one`
`realize_liftAt` 📖	mathematical	—	`realize` `liftAt`	—	`realize_relabel`
`realize_relabel` 📖	mathematical	—	`realize` `relabel`	—	—
`realize_restrictVar` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `varFinset`	`realize` `restrictVar`	—	`Finset.mem_singleton_self`
`realize_restrictVar'` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `varFinset`	`realize` `Set.Elem` `Set.instMembership` `restrictVar` `Set.inclusion`	—	`realize_restrictVar`
`realize_restrictVarLeft` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `varFinsetLeft`	`realize` `restrictVarLeft`	—	`Finset.mem_singleton_self`
`realize_restrictVarLeft'` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `varFinsetLeft`	`realize` `Set.Elem` `Set.instMembership` `restrictVarLeft` `Set.inclusion`	—	`realize_restrictVarLeft`
`realize_subst` 📖	mathematical	—	`realize` `subst`	—	—
`realize_substFunc` 📖	mathematical	`realize` `FirstOrder.Language.Functions.term`	`substFunc`	—	`realize_subst` `realize_function_term`
`realize_var` 📖	mathematical	—	`realize` `var`	—	—
`realize_varsToConstants` 📖	mathematical	—	`realize` `FirstOrder.Language.withConstants` `varsToConstants` `FirstOrder.Language.constantMap` `FirstOrder.Language.con`	—	`realize_constants` `FirstOrder.Language.withConstants_funMap_sumInl`

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
`Model` 📖	CompData	44 math math: `FirstOrder.Language.ElementarilyEquivalent.theory_model_iff`, `FirstOrder.Field.modelField_of_modelACF`, `FirstOrder.Language.ElementarySubstructure.theory_model`, `ModelType.subtheoryModel_models`, `model_union_iff`, `FirstOrder.Language.model_infiniteTheory`, `FirstOrder.Language.model_partialOrder`, `FirstOrder.Language.dlo_age`, `FirstOrder.Language.model_preorder`, `FirstOrder.Language.instModelLinearOrderTheoryOfDlo`, `FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed`, `model_iff`, `FirstOrder.Language.model_infiniteTheory_iff`, `ModelType.is_model`, `FirstOrder.Language.instModelPartialOrderTheoryOfLinearOrderTheory`, `IsUniversal.models_of_embedding`, `FirstOrder.Language.instModelPreorderTheoryOfPartialOrderTheory`, `FirstOrder.Language.isFraisse_finite_linear_order`, `FirstOrder.Language.model_nonempty`, `FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo`, `model_singleton_iff`, `FirstOrder.Language.model_linearOrder`, `FirstOrder.Language.ElementarilyEquivalent.theory_model`, `FirstOrder.Language.simpleGraph_model`, `model_insert_iff`, `model_iff_subset_completeTheory`, `FirstOrder.Language.model_distinctConstantsTheory`, `FirstOrder.Language.ElementarySubstructure.theory_model_iff`, `FirstOrder.Field.instModelField`, `FirstOrder.Language.model_dlo`, `FirstOrder.Field.model_hasChar_of_charP`, `FirstOrder.Field.instModelFieldOfCharOfACF`, `FirstOrder.Language.ElementaryEmbedding.theory_model_iff`, `FirstOrder.Language.model_nonemptyTheory_iff`, `simpleGraph_model_iff`, `FirstOrder.Language.LHom.onTheory_model`, `FirstOrder.Field.model_fieldOfChar_of_charP`, `FirstOrder.Language.StrongHomClass.theory_model`, `FirstOrder.Language.model_empty`, `Model.mono`, `FirstOrder.Language.Substructure.models_of_isUniversal`, `Model.union`, `FirstOrder.Field.charP_iff_model_fieldOfChar`, `FirstOrder.Language.model_completeTheory`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`model_iff` 📖	mathematical	—	`Model` `FirstOrder.Language.Sentence.Realize`	—	`Model.realize_of_mem`
`model_iff_subset_completeTheory` 📖	mathematical	—	`Model` `FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence` `FirstOrder.Language.completeTheory`	—	`model_iff`
`model_insert_iff` 📖	mathematical	—	`Model` `FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instInsert` `FirstOrder.Language.Sentence.Realize`	—	`Set.insert_eq` `model_union_iff` `model_singleton_iff`
`model_singleton_iff` 📖	mathematical	—	`Model` `FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instSingletonSet` `FirstOrder.Language.Sentence.Realize`	—	—
`model_union_iff` 📖	mathematical	—	`Model` `FirstOrder.Language.Theory` `Set.instUnion` `FirstOrder.Language.Sentence`	—	`Model.mono` `Set.subset_union_left` `Set.subset_union_right` `Model.union`
`realize_sentence_of_mem` 📖	mathematical	`FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instMembership`	`FirstOrder.Language.Sentence.Realize`	—	`Model.realize_of_mem`

FirstOrder.Language.Theory.Model

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence`	`FirstOrder.Language.Theory.Model`	—	`FirstOrder.Language.Theory.realize_sentence_of_mem`
`realize_of_mem` 📖	mathematical	`FirstOrder.Language.Sentence` `FirstOrder.Language.Theory` `Set.instMembership`	`FirstOrder.Language.Sentence.Realize`	—	—
`union` 📖	mathematical	—	`FirstOrder.Language.Theory.Model` `FirstOrder.Language.Theory` `Set.instUnion` `FirstOrder.Language.Sentence`	—	—

FirstOrder.Language.Theory.completeTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subset` 📖	mathematical	—	`FirstOrder.Language.Theory` `Set.instHasSubset` `FirstOrder.Language.Sentence` `FirstOrder.Language.completeTheory`	—	`FirstOrder.Language.Theory.model_iff_subset_completeTheory`

---

← Back to Index