LanguageMap

📁 Source: Mathlib/ModelTheory/LanguageMap.lean

Statistics

Metric	Count
Definitions `LEquiv`, `addEmptyConstants`, `instInhabited`, `invLHom`, `refl`, `toLHom`, `trans`, `LHom`, `IsExpansionOn`, `addConstants`, `comp`, `constantsOnMap`, `defaultExpansion`, `id`, `instInhabited`, `instUniqueOfIsAlgebraicOfIsRelational`, `ofIsEmpty`, `onFunction`, `onRelation`, `reduct`, `sumElim`, `sumInl`, `sumInr`, `sumMap`, `con`, `constantsOn`, `structure`, `constantsOnFunc`, `constantsOnSelfStructure`, `lhomWithConstants`, `lhomWithConstantsMap`, `paramsStructure`, `withConstants`, `withConstantsSelfStructure`, `withConstantsStructure`, `«term_→ᴸ_»`, `«term_≃ᴸ_»`, `«term_[[_]]»`	38
Theorems `addEmptyConstants_invLHom`, `addEmptyConstants_toLHom`, `left_inv`, `refl_invLHom`, `refl_toLHom`, `right_inv`, `symm_invLHom`, `symm_toLHom`, `trans_invLHom`, `trans_toLHom`, `isExpansionOn_default`, `onFunction`, `onRelation`, `map_onFunction`, `map_onRelation`, `comp_assoc`, `comp_id`, `comp_onFunction`, `comp_onRelation`, `comp_sumElim`, `funMap_sumInl`, `funMap_sumInr`, `funext`, `funext_iff`, `id_comp`, `id_isExpansionOn`, `id_onFunction`, `id_onRelation`, `isExpansionOn_reduct`, `map_constants_comp_sumInl`, `map_onFunction`, `map_onRelation`, `ofIsEmpty_isExpansionOn`, `ofIsEmpty_onFunction`, `ofIsEmpty_onRelation`, `sumElim_comp_inl`, `sumElim_comp_inr`, `sumElim_inl_inr`, `sumElim_isExpansionOn`, `sumElim_onFunction`, `sumElim_onRelation`, `sumInl_injective`, `sumInl_isExpansionOn`, `sumInl_onFunction`, `sumInl_onRelation`, `sumInr_injective`, `sumInr_isExpansionOn`, `sumInr_onFunction`, `sumInr_onRelation`, `sumMap_comp_inl`, `sumMap_comp_inr`, `sumMap_isExpansionOn`, `sumMap_onFunction`, `sumMap_onRelation`, `addConstants_expansion`, `addEmptyConstants_is_expansion_on'`, `addEmptyConstants_symm_isExpansionOn`, `card_constantsOn`, `card_withConstants`, `coe_con`, `constantsOnMap_inclusion_isExpansionOn`, `constantsOnMap_isExpansionOn`, `constantsOn_Functions`, `constantsOn_Relations`, `constantsOn_constants`, `isAlgebraic_constantsOn`, `isEmpty_functions_constantsOn_succ`, `isRelational_constantsOn`, `lhomWithConstants_injective`, `lhomWithConstants_onFunction`, `lhomWithConstants_onRelation`, `map_constants_inclusion_isExpansionOn`, `withConstants_expansion`, `withConstants_funMap_sumInl`, `withConstants_funMap_sumInr`, `withConstants_relMap_sumInl`, `withConstants_self_expansion`	77
Total	115

FirstOrder

Definitions

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

FirstOrder.Language

Definitions

Name	Category	Theorems
`LEquiv` 📖	CompData	—
`LHom` 📖	CompData	—
`con` 📖	CompOp	10 math math: `coe_con`, `Term.realize_constantsToVars`, `Term.realize_constantsVarsEquivLeft`, `Formula.realize_equivSentence_symm_con`, `Term.realize_con`, `model_distinctConstantsTheory`, `withConstants_funMap_sumInr`, `BoundedFormula.realize_constantsVarsEquiv`, `Term.realize_varsToConstants`, `Formula.realize_equivSentence`
`constantsOn` 📖	CompOp	15 math math: `isRelational_constantsOn`, `constantsOnMap_isExpansionOn`, `constantsOn_Relations`, `constantsOn_Functions`, `constantsOnMap_inclusion_isExpansionOn`, `LEquiv.addEmptyConstants_invLHom`, `withConstants_funMap_sumInl`, `constantsOn_constants`, `LHom.map_constants_comp_sumInl`, `withConstants_relMap_sumInl`, `card_constantsOn`, `withConstants_funMap_sumInr`, `BoundedFormula.instCountableSymbolsConstantsOn`, `isAlgebraic_constantsOn`, `isEmpty_functions_constantsOn_succ`
`constantsOnFunc` 📖	CompOp	1 math math: `constantsOn_Functions`
`constantsOnSelfStructure` 📖	CompOp	—
`lhomWithConstants` 📖	CompOp	16 math math: `lhomWithConstants_onRelation`, `LEquiv.addEmptyConstants_toLHom`, `withConstants_expansion`, `Theory.CompleteType.subset'`, `withConstants_self_expansion`, `Substructure.reduct_withConstants`, `Theory.models_formula_iff_onTheory_models_equivSentence`, `lhomWithConstants_onFunction`, `LHom.map_constants_comp_sumInl`, `Theory.CompleteType.setOf_mem_eq_univ_iff`, `lhomWithConstants_injective`, `Theory.CompleteType.setOf_subset_eq_empty_iff`, `Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite`, `Theory.CompleteType.setOf_subset_eq_univ_iff`, `Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le`, `Theory.CompleteType.subset`
`lhomWithConstantsMap` 📖	CompOp	2 math math: `LHom.map_constants_comp_sumInl`, `map_constants_inclusion_isExpansionOn`
`paramsStructure` 📖	CompOp	16 math math: `Set.definable_iff_empty_definable_with_params`, `Set.TermDefinable₁.const`, `Set.termDefinable_empty_withConstants_iff`, `coe_con`, `addEmptyConstants_symm_isExpansionOn`, `constantsOnMap_inclusion_isExpansionOn`, `Substructure.reduct_withConstants`, `Set.termDefinable₁_iff_exists_term`, `Term.realize_con`, `Substructure.coe_withConstants`, `Substructure.mem_withConstants`, `addEmptyConstants_is_expansion_on'`, `Set.TermDefinable.const`, `Substructure.closure_withConstants_eq`, `Substructure.subset_closure_withConstants`, `map_constants_inclusion_isExpansionOn`
`withConstants` 📖	CompOp	70 math math: `Theory.CompleteType.compl_setOf_mem`, `Theory.CompleteType.mem_or_not_mem`, `Set.definable_iff_empty_definable_with_params`, `directed_distinctConstantsTheory`, `Set.TermDefinable₁.const`, `lhomWithConstants_onRelation`, `Set.termDefinable_empty_withConstants_iff`, `coe_con`, `Term.constantsVarsEquiv_symm_apply`, `LEquiv.addEmptyConstants_toLHom`, `CompleteType.isTopologicalBasis_range_typesWith`, `Term.constantsVarsEquivLeft_apply`, `addEmptyConstants_symm_isExpansionOn`, `Formula.equivSentence_not`, `BoundedFormula.instCountableSymbolsWithConstants`, `withConstants_expansion`, `Term.realize_constantsToVars`, `Theory.CompleteType.subset'`, `LEquiv.addEmptyConstants_invLHom`, `withConstants_self_expansion`, `Formula.equivSentence_inf`, `Substructure.reduct_withConstants`, `Term.constantsVarsEquivLeft_symm_apply`, `distinctConstantsTheory_mono`, `Term.realize_constantsVarsEquivLeft`, `Set.termDefinable₁_iff_exists_term`, `Theory.models_formula_iff_onTheory_models_equivSentence`, `Term.constantsVarsEquiv_apply`, `withConstants_funMap_sumInl`, `Formula.realize_equivSentence_symm_con`, `monotone_distinctConstantsTheory`, `lhomWithConstants_onFunction`, `LHom.map_constants_comp_sumInl`, `Term.realize_con`, `Theory.CompleteType.formula_mem_typeOf`, `Theory.CompleteType.setOf_mem_eq_univ_iff`, `model_distinctConstantsTheory`, `withConstants_relMap_sumInl`, `Substructure.coe_withConstants`, `lhomWithConstants_injective`, `distinctConstantsTheory_eq_iUnion`, `Theory.CompleteType.isMaximal'`, `ElementaryEmbedding.ofModelsElementaryDiagram_toFun`, `Substructure.mem_withConstants`, `addEmptyConstants_is_expansion_on'`, `withConstants_funMap_sumInr`, `Theory.CompleteType.not_mem_iff`, `Set.TermDefinable.const`, `Theory.CompleteType.iInter_setOf_subset`, `Theory.CompleteType.setOf_subset_eq_empty_iff`, `Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite`, `card_withConstants`, `BoundedFormula.realize_constantsVarsEquiv`, `Theory.CompleteType.mem_typeOf`, `Substructure.closure_withConstants_eq`, `Theory.CompleteType.setOf_subset_eq_univ_iff`, `Theory.CompleteType.toList_foldr_inf_mem`, `Substructure.subset_closure_withConstants`, `Theory.CompleteType.typesWith_not`, `Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le`, `Theory.CompleteType.isMaximal`, `Theory.CompleteType.typesWith_inf`, `addConstants_expansion`, `Theory.CompleteType.typesWith_top`, `map_constants_inclusion_isExpansionOn`, `Term.realize_varsToConstants`, `Formula.realize_equivSentence_symm`, `Formula.realize_equivSentence`, `Theory.CompleteType.subset`, `Theory.CompleteType.mem_typesWith_iff`
`withConstantsSelfStructure` 📖	CompOp	1 math math: `withConstants_self_expansion`
`withConstantsStructure` 📖	CompOp	19 math math: `Set.definable_iff_empty_definable_with_params`, `Set.TermDefinable₁.const`, `Set.termDefinable_empty_withConstants_iff`, `coe_con`, `addEmptyConstants_symm_isExpansionOn`, `withConstants_expansion`, `Substructure.reduct_withConstants`, `Set.termDefinable₁_iff_exists_term`, `Term.realize_con`, `Substructure.coe_withConstants`, `Substructure.mem_withConstants`, `addEmptyConstants_is_expansion_on'`, `withConstants_funMap_sumInr`, `Set.TermDefinable.const`, `Substructure.closure_withConstants_eq`, `Substructure.subset_closure_withConstants`, `addConstants_expansion`, `map_constants_inclusion_isExpansionOn`, `Formula.realize_equivSentence_symm`
`«term_→ᴸ_»` 📖	CompOp	—
`«term_≃ᴸ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addConstants_expansion` 📖	mathematical	—	`LHom.IsExpansionOn` `withConstants` `LHom.addConstants` `withConstantsStructure`	—	`LHom.sumMap_isExpansionOn` `LHom.id_isExpansionOn`
`addEmptyConstants_is_expansion_on'` 📖	mathematical	—	`LHom.IsExpansionOn` `withConstants` `Set.Elem` `Set` `Set.instEmptyCollection` `LEquiv.toLHom` `LEquiv.addEmptyConstants` `Set.instIsEmptyElemEmptyCollection` `withConstantsStructure` `paramsStructure`	—	`withConstants_expansion`
`addEmptyConstants_symm_isExpansionOn` 📖	mathematical	—	`LHom.IsExpansionOn` `withConstants` `Set.Elem` `Set` `Set.instEmptyCollection` `LEquiv.toLHom` `LEquiv.symm` `LEquiv.addEmptyConstants` `Set.instIsEmptyElemEmptyCollection` `withConstantsStructure` `paramsStructure`	—	`LHom.sumElim_isExpansionOn` `isAlgebraic_constantsOn` `isRelational_constantsOn` `Set.instIsEmptyElemEmptyCollection` `LHom.id_isExpansionOn` `LHom.ofIsEmpty_isExpansionOn`
`card_constantsOn` 📖	mathematical	—	`card` `constantsOn`	—	`card_eq_card_functions_add_card_relations` `Cardinal.lift_uzero` `Cardinal.sum_nat_eq_add_sum_succ` `Cardinal.mk_eq_zero` `PEmpty.instIsEmpty` `Cardinal.sum_const` `Cardinal.mk_eq_aleph0` `instCountableNat` `instInfiniteNat` `Cardinal.lift_aleph0` `MulZeroClass.mul_zero` `add_zero` `Empty.instIsEmpty` `Cardinal.lift_zero`
`card_withConstants` 📖	mathematical	—	`card` `withConstants` `Cardinal` `Cardinal.instAdd` `Cardinal.lift`	—	`withConstants.eq_1` `card_sum` `card_constantsOn`
`coe_con` 📖	mathematical	—	`constantMap` `withConstants` `Set.Elem` `withConstantsStructure` `paramsStructure` `con` `Set` `Set.instMembership`	—	—
`constantsOnMap_inclusion_isExpansionOn` 📖	mathematical	`Set` `Set.instHasSubset`	`LHom.IsExpansionOn` `constantsOn` `Set.Elem` `LHom.constantsOnMap` `Set.inclusion` `paramsStructure`	—	`constantsOnMap_isExpansionOn`
`constantsOnMap_isExpansionOn` 📖	mathematical	—	`LHom.IsExpansionOn` `constantsOn` `LHom.constantsOnMap` `constantsOn.structure`	—	`isEmpty_functions_constantsOn_succ` `isAlgebraic_constantsOn`
`constantsOn_Functions` 📖	mathematical	—	`Functions` `constantsOn` `constantsOnFunc`	—	—
`constantsOn_Relations` 📖	mathematical	—	`Relations` `constantsOn`	—	—
`constantsOn_constants` 📖	mathematical	—	`Constants` `constantsOn`	—	—
`isAlgebraic_constantsOn` 📖	mathematical	—	`IsAlgebraic` `constantsOn`	—	`Empty.instIsEmpty`
`isEmpty_functions_constantsOn_succ` 📖	mathematical	—	`IsEmpty` `Functions` `constantsOn`	—	`PEmpty.instIsEmpty`
`isRelational_constantsOn` 📖	mathematical	—	`IsRelational` `constantsOn`	—	`isEmpty_functions_constantsOn_succ`
`lhomWithConstants_injective` 📖	mathematical	—	`LHom.Injective` `withConstants` `lhomWithConstants`	—	`LHom.sumInl_injective`
`lhomWithConstants_onFunction` 📖	mathematical	—	`LHom.onFunction` `withConstants` `lhomWithConstants` `Functions`	—	—
`lhomWithConstants_onRelation` 📖	mathematical	—	`LHom.onRelation` `withConstants` `lhomWithConstants` `Relations`	—	—
`map_constants_inclusion_isExpansionOn` 📖	mathematical	`Set` `Set.instHasSubset`	`LHom.IsExpansionOn` `withConstants` `Set.Elem` `lhomWithConstantsMap` `Set.inclusion` `withConstantsStructure` `paramsStructure`	—	`LHom.sumMap_isExpansionOn` `LHom.id_isExpansionOn` `constantsOnMap_inclusion_isExpansionOn`
`withConstants_expansion` 📖	mathematical	—	`LHom.IsExpansionOn` `withConstants` `lhomWithConstants` `withConstantsStructure`	—	—
`withConstants_funMap_sumInl` 📖	mathematical	—	`Structure.funMap` `withConstants` `Functions` `constantsOn`	—	`LHom.map_onFunction`
`withConstants_funMap_sumInr` 📖	mathematical	—	`Structure.funMap` `withConstants` `withConstantsStructure` `Functions` `constantsOn` `constantMap` `con`	—	`Fin.isEmpty'` `Unique.eq_default` `LHom.map_onFunction` `LHom.sumInr_isExpansionOn`
`withConstants_relMap_sumInl` 📖	mathematical	—	`Structure.RelMap` `withConstants` `Relations` `constantsOn`	—	`LHom.map_onRelation`
`withConstants_self_expansion` 📖	mathematical	—	`LHom.IsExpansionOn` `withConstants` `lhomWithConstants` `withConstantsSelfStructure`	—	—

FirstOrder.Language.LEquiv

Definitions

Name	Category	Theorems
`addEmptyConstants` 📖	CompOp	4 math math: `addEmptyConstants_toLHom`, `FirstOrder.Language.addEmptyConstants_symm_isExpansionOn`, `addEmptyConstants_invLHom`, `FirstOrder.Language.addEmptyConstants_is_expansion_on'`
`instInhabited` 📖	CompOp	—
`invLHom` 📖	CompOp	10 math math: `onTerm_symm_apply`, `right_inv`, `symm_toLHom`, `trans_invLHom`, `symm_invLHom`, `addEmptyConstants_invLHom`, `onBoundedFormula_symm_apply`, `onSentence_symm_apply`, `refl_invLHom`, `left_inv`
`refl` 📖	CompOp	2 math math: `refl_toLHom`, `refl_invLHom`
`toLHom` 📖	CompOp	13 math math: `right_inv`, `addEmptyConstants_toLHom`, `FirstOrder.Language.addEmptyConstants_symm_isExpansionOn`, `onFormula_apply`, `symm_toLHom`, `onSentence_apply`, `symm_invLHom`, `trans_toLHom`, `FirstOrder.Language.addEmptyConstants_is_expansion_on'`, `refl_toLHom`, `onTerm_apply`, `onBoundedFormula_apply`, `left_inv`
`trans` 📖	CompOp	2 math math: `trans_invLHom`, `trans_toLHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEmptyConstants_invLHom` 📖	mathematical	—	`invLHom` `FirstOrder.Language.withConstants` `addEmptyConstants` `FirstOrder.Language.LHom.sumElim` `FirstOrder.Language.LHom.id` `FirstOrder.Language.constantsOn` `FirstOrder.Language.LHom.ofIsEmpty` `FirstOrder.Language.isAlgebraic_constantsOn` `FirstOrder.Language.isRelational_constantsOn`	—	—
`addEmptyConstants_toLHom` 📖	mathematical	—	`toLHom` `FirstOrder.Language.withConstants` `addEmptyConstants` `FirstOrder.Language.lhomWithConstants`	—	—
`left_inv` 📖	mathematical	—	`FirstOrder.Language.LHom.comp` `invLHom` `toLHom` `FirstOrder.Language.LHom.id`	—	—
`refl_invLHom` 📖	mathematical	—	`invLHom` `refl` `FirstOrder.Language.LHom.id`	—	—
`refl_toLHom` 📖	mathematical	—	`toLHom` `refl` `FirstOrder.Language.LHom.id`	—	—
`right_inv` 📖	mathematical	—	`FirstOrder.Language.LHom.comp` `toLHom` `invLHom` `FirstOrder.Language.LHom.id`	—	—
`symm_invLHom` 📖	mathematical	—	`invLHom` `symm` `toLHom`	—	—
`symm_toLHom` 📖	mathematical	—	`toLHom` `symm` `invLHom`	—	—
`trans_invLHom` 📖	mathematical	—	`invLHom` `trans` `FirstOrder.Language.LHom.comp`	—	—
`trans_toLHom` 📖	mathematical	—	`toLHom` `trans` `FirstOrder.Language.LHom.comp`	—	—

FirstOrder.Language.LHom

Definitions

Name	Category	Theorems
`IsExpansionOn` 📖	CompData	18 math math: `sumElim_isExpansionOn`, `FirstOrder.Language.constantsOnMap_isExpansionOn`, `FirstOrder.Language.addEmptyConstants_symm_isExpansionOn`, `sumMap_isExpansionOn`, `ofIsEmpty_isExpansionOn`, `FirstOrder.Language.withConstants_expansion`, `FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder`, `FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn`, `FirstOrder.Language.withConstants_self_expansion`, `sumInl_isExpansionOn`, `FirstOrder.Language.addEmptyConstants_is_expansion_on'`, `FirstOrder.Language.orderedStructure_iff`, `Injective.isExpansionOn_default`, `id_isExpansionOn`, `isExpansionOn_reduct`, `FirstOrder.Language.addConstants_expansion`, `FirstOrder.Language.map_constants_inclusion_isExpansionOn`, `sumInr_isExpansionOn`
`addConstants` 📖	CompOp	1 math math: `FirstOrder.Language.addConstants_expansion`
`comp` 📖	CompOp	17 math math: `sumMap_comp_inl`, `FirstOrder.Language.LEquiv.right_inv`, `comp_onFunction`, `sumElim_comp_inr`, `id_comp`, `FirstOrder.Language.LEquiv.trans_invLHom`, `comp_assoc`, `FirstOrder.Language.LEquiv.trans_toLHom`, `comp_onTerm`, `comp_onRelation`, `comp_sumElim`, `comp_onBoundedFormula`, `sumElim_comp_inl`, `map_constants_comp_sumInl`, `comp_id`, `sumMap_comp_inr`, `FirstOrder.Language.LEquiv.left_inv`
`constantsOnMap` 📖	CompOp	2 math math: `FirstOrder.Language.constantsOnMap_isExpansionOn`, `FirstOrder.Language.constantsOnMap_inclusion_isExpansionOn`
`defaultExpansion` 📖	CompOp	2 math math: `FirstOrder.Language.Theory.ModelType.defaultExpansion_struc`, `Injective.isExpansionOn_default`
`id` 📖	CompOp	14 math math: `id_onRelation`, `FirstOrder.Language.LEquiv.right_inv`, `sumElim_inl_inr`, `id_comp`, `FirstOrder.Language.orderLHom_order`, `FirstOrder.Language.LEquiv.addEmptyConstants_invLHom`, `comp_id`, `FirstOrder.Language.LEquiv.refl_toLHom`, `id_onFunction`, `id_onBoundedFormula`, `id_isExpansionOn`, `FirstOrder.Language.LEquiv.refl_invLHom`, `id_onTerm`, `FirstOrder.Language.LEquiv.left_inv`
`instInhabited` 📖	CompOp	—
`instUniqueOfIsAlgebraicOfIsRelational` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	4 math math: `ofIsEmpty_isExpansionOn`, `ofIsEmpty_onRelation`, `FirstOrder.Language.LEquiv.addEmptyConstants_invLHom`, `ofIsEmpty_onFunction`
`onFunction` 📖	CompOp	13 math math: `Injective.onFunction`, `sumElim_onFunction`, `sumMap_onFunction`, `comp_onFunction`, `map_onFunction`, `IsExpansionOn.map_onFunction`, `sumInr_onFunction`, `sumInl_onFunction`, `FirstOrder.Language.lhomWithConstants_onFunction`, `FirstOrder.Language.orderLHom_onFunction`, `id_onFunction`, `funext_iff`, `ofIsEmpty_onFunction`
`onRelation` 📖	CompOp	14 math math: `FirstOrder.Language.orderLHom_leSymb`, `id_onRelation`, `FirstOrder.Language.lhomWithConstants_onRelation`, `ofIsEmpty_onRelation`, `sumInr_onRelation`, `comp_onRelation`, `IsExpansionOn.map_onRelation`, `sumElim_onRelation`, `FirstOrder.Language.orderLHom_onRelation`, `map_onRelation`, `sumInl_onRelation`, `funext_iff`, `sumMap_onRelation`, `Injective.onRelation`
`reduct` 📖	CompOp	2 math math: `FirstOrder.Language.Theory.ModelType.reduct_struc`, `isExpansionOn_reduct`
`sumElim` 📖	CompOp	8 math math: `sumElim_onFunction`, `sumElim_isExpansionOn`, `sumElim_comp_inr`, `sumElim_inl_inr`, `FirstOrder.Language.LEquiv.addEmptyConstants_invLHom`, `comp_sumElim`, `sumElim_comp_inl`, `sumElim_onRelation`
`sumInl` 📖	CompOp	9 math math: `sumInl_injective`, `sumMap_comp_inl`, `sumElim_inl_inr`, `FirstOrder.Language.Substructure.skolem₁_reduct_isElementary`, `sumElim_comp_inl`, `sumInl_onFunction`, `map_constants_comp_sumInl`, `sumInl_isExpansionOn`, `sumInl_onRelation`
`sumInr` 📖	CompOp	7 math math: `sumElim_comp_inr`, `sumElim_inl_inr`, `sumInr_onRelation`, `sumInr_onFunction`, `sumMap_comp_inr`, `sumInr_isExpansionOn`, `sumInr_injective`
`sumMap` 📖	CompOp	5 math math: `sumMap_comp_inl`, `sumMap_onFunction`, `sumMap_isExpansionOn`, `sumMap_comp_inr`, `sumMap_onRelation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_onFunction` 📖	mathematical	—	`onFunction` `comp`	—	—
`comp_onRelation` 📖	mathematical	—	`onRelation` `comp`	—	—
`comp_sumElim` 📖	mathematical	—	`comp` `FirstOrder.Language.sum` `sumElim`	—	`funext`
`funMap_sumInl` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.sum` `FirstOrder.Language.Functions`	—	`map_onFunction`
`funMap_sumInr` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.sum` `FirstOrder.Language.Functions`	—	`map_onFunction`
`funext` 📖	—	`onFunction` `onRelation`	—	—	—
`funext_iff` 📖	mathematical	—	`onFunction` `onRelation`	—	`funext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`id_isExpansionOn` 📖	mathematical	—	`IsExpansionOn` `id`	—	—
`id_onFunction` 📖	mathematical	—	`onFunction` `id` `FirstOrder.Language.Functions`	—	—
`id_onRelation` 📖	mathematical	—	`onRelation` `id` `FirstOrder.Language.Relations`	—	—
`isExpansionOn_reduct` 📖	mathematical	—	`IsExpansionOn` `reduct`	—	—
`map_constants_comp_sumInl` 📖	mathematical	—	`comp` `FirstOrder.Language.withConstants` `FirstOrder.Language.lhomWithConstantsMap` `sumInl` `FirstOrder.Language.constantsOn` `FirstOrder.Language.lhomWithConstants`	—	`funext`
`map_onFunction` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `onFunction`	—	`IsExpansionOn.map_onFunction`
`map_onRelation` 📖	mathematical	—	`FirstOrder.Language.Structure.RelMap` `onRelation`	—	`IsExpansionOn.map_onRelation`
`ofIsEmpty_isExpansionOn` 📖	mathematical	`FirstOrder.Language.IsAlgebraic` `FirstOrder.Language.IsRelational`	`IsExpansionOn` `ofIsEmpty`	—	—
`ofIsEmpty_onFunction` 📖	mathematical	`FirstOrder.Language.IsAlgebraic` `FirstOrder.Language.IsRelational`	`onFunction` `ofIsEmpty` `isEmptyElim` `FirstOrder.Language.Functions`	—	—
`ofIsEmpty_onRelation` 📖	mathematical	`FirstOrder.Language.IsAlgebraic` `FirstOrder.Language.IsRelational`	`onRelation` `ofIsEmpty` `isEmptyElim` `FirstOrder.Language.Relations`	—	—
`sumElim_comp_inl` 📖	mathematical	—	`comp` `FirstOrder.Language.sum` `sumElim` `sumInl`	—	`funext`
`sumElim_comp_inr` 📖	mathematical	—	`comp` `FirstOrder.Language.sum` `sumElim` `sumInr`	—	`funext`
`sumElim_inl_inr` 📖	mathematical	—	`sumElim` `FirstOrder.Language.sum` `sumInl` `sumInr` `id`	—	`funext`
`sumElim_isExpansionOn` 📖	mathematical	—	`IsExpansionOn` `FirstOrder.Language.sum` `sumElim` `FirstOrder.Language.sumStructure`	—	`map_onFunction` `map_onRelation`
`sumElim_onFunction` 📖	mathematical	—	`onFunction` `FirstOrder.Language.sum` `sumElim` `FirstOrder.Language.Functions`	—	—
`sumElim_onRelation` 📖	mathematical	—	`onRelation` `FirstOrder.Language.sum` `sumElim` `FirstOrder.Language.Relations`	—	—
`sumInl_injective` 📖	mathematical	—	`Injective` `FirstOrder.Language.sum` `sumInl`	—	`Sum.inl_injective`
`sumInl_isExpansionOn` 📖	mathematical	—	`IsExpansionOn` `FirstOrder.Language.sum` `sumInl` `FirstOrder.Language.sumStructure`	—	—
`sumInl_onFunction` 📖	mathematical	—	`onFunction` `FirstOrder.Language.sum` `sumInl` `FirstOrder.Language.Functions`	—	—
`sumInl_onRelation` 📖	mathematical	—	`onRelation` `FirstOrder.Language.sum` `sumInl` `FirstOrder.Language.Relations`	—	—
`sumInr_injective` 📖	mathematical	—	`Injective` `FirstOrder.Language.sum` `sumInr`	—	`Sum.inr_injective`
`sumInr_isExpansionOn` 📖	mathematical	—	`IsExpansionOn` `FirstOrder.Language.sum` `sumInr` `FirstOrder.Language.sumStructure`	—	—
`sumInr_onFunction` 📖	mathematical	—	`onFunction` `FirstOrder.Language.sum` `sumInr` `FirstOrder.Language.Functions`	—	—
`sumInr_onRelation` 📖	mathematical	—	`onRelation` `FirstOrder.Language.sum` `sumInr` `FirstOrder.Language.Relations`	—	—
`sumMap_comp_inl` 📖	mathematical	—	`comp` `FirstOrder.Language.sum` `sumMap` `sumInl`	—	`funext`
`sumMap_comp_inr` 📖	mathematical	—	`comp` `FirstOrder.Language.sum` `sumMap` `sumInr`	—	`funext`
`sumMap_isExpansionOn` 📖	mathematical	—	`IsExpansionOn` `FirstOrder.Language.sum` `sumMap` `FirstOrder.Language.sumStructure`	—	`map_onFunction` `map_onRelation`
`sumMap_onFunction` 📖	mathematical	—	`onFunction` `FirstOrder.Language.sum` `sumMap` `FirstOrder.Language.Functions`	—	—
`sumMap_onRelation` 📖	mathematical	—	`onRelation` `FirstOrder.Language.sum` `sumMap` `FirstOrder.Language.Relations`	—	—

FirstOrder.Language.LHom.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExpansionOn_default` 📖	mathematical	`FirstOrder.Language.LHom.Injective`	`FirstOrder.Language.LHom.IsExpansionOn` `FirstOrder.Language.LHom.defaultExpansion`	—	`onFunction` `onRelation`
`onFunction` 📖	mathematical	`FirstOrder.Language.LHom.Injective`	`FirstOrder.Language.Functions` `FirstOrder.Language.LHom.onFunction`	—	—
`onRelation` 📖	mathematical	`FirstOrder.Language.LHom.Injective`	`FirstOrder.Language.Relations` `FirstOrder.Language.LHom.onRelation`	—	—

FirstOrder.Language.LHom.IsExpansionOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_onFunction` 📖	mathematical	—	`FirstOrder.Language.Structure.funMap` `FirstOrder.Language.LHom.onFunction`	—	—
`map_onRelation` 📖	mathematical	—	`FirstOrder.Language.Structure.RelMap` `FirstOrder.Language.LHom.onRelation`	—	—

FirstOrder.Language.constantsOn

Definitions

Name	Category	Theorems
`structure` 📖	CompOp	2 math math: `FirstOrder.Language.constantsOnMap_isExpansionOn`, `FirstOrder.Language.Formula.realize_equivSentence_symm`

---

← Back to Index