DirectLimit

📁 Source: Mathlib/ModelTheory/DirectLimit.lean

Statistics

Metric	Count
Definitions DirectLimit, DirectLimit, DirectLimit, Equiv_iSup, equiv_lift, instStructureDirectLimit, liftInclusion, of, prestructure, setoid, sigmaStructure, unify, natLERec, mk, instInhabitedDirectLimitOfDefault, DirectLimit, DirectLimit	17
Theorems Equiv_isup_of_apply, Equiv_isup_symm_inclusion, Equiv_isup_symm_inclusion_apply, cg, cg', comp_unify, equiv_iff, equiv_lift_of, exists_fg_substructure_in_Sigma, exists_of, exists_quotient_mk'_sigma_mk'_eq, exists_unify_eq, funMap_equiv_unify, funMap_quotient_mk'_sigma_mk', funMap_unify_equiv, iSup_range_of_eq_top, inductionOn, liftInclusion_of, lift_of, lift_quotient_mk'_sigma_mk', lift_unique, of_apply, of_f, rangeLiftInclusion, range_lift, relMap_equiv_unify, relMap_quotient_mk'_sigma_mk', relMap_unify_equiv, unify_sigma_mk_self, coe_natLERec, map_map, map_self, directedSystem, instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion	34
Total	51

AddCommGroup

Definitions

Name	Category	Theorems
DirectLimit 📖	CompOp	11 math math: DirectLimit.lift_of', DirectLimit.of_f, DirectLimit.congr_apply_of, DirectLimit.congr_symm_apply_of, DirectLimit.lift_comp_of, DirectLimit.lift_of, DirectLimit.lift_injective, DirectLimit.map_id, DirectLimit.map_comp, DirectLimit.hom_ext_iff, DirectLimit.map_apply_of

FirstOrder.Language

Definitions

Name	Category	Theorems
DirectLimit 📖	CompOp	17 math math: DirectLimit.of_f, DirectLimit.lift_unique, DirectLimit.liftInclusion_of, DirectLimit.cg, DirectLimit.Equiv_isup_symm_inclusion, DirectLimit.lift_quotient_mk'_sigma_mk', DirectLimit.lift_of, DirectLimit.of_apply, age_directLimit, DirectLimit.equiv_lift_of, DirectLimit.Equiv_isup_of_apply, DirectLimit.iSup_range_of_eq_top, DirectLimit.Equiv_isup_symm_inclusion_apply, DirectLimit.cg', DirectLimit.exists_of, DirectLimit.range_lift, DirectLimit.rangeLiftInclusion
instInhabitedDirectLimitOfDefault 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion 📖	mathematical	—	DirectedSystem Substructure SetLike.instMembership Substructure.instSetLike DFunLike.coe OrderHom PartialOrder.toPreorder Substructure.instPartialOrder OrderHom.instFunLike Embedding Substructure.inducedStructure Embedding.funLike Substructure.inclusion OrderHom.monotone	—	OrderHom.monotone le_rfl

FirstOrder.Language.DirectLimit

Definitions

Name	Category	Theorems
Equiv_iSup 📖	CompOp	3 math math: Equiv_isup_symm_inclusion, Equiv_isup_of_apply, Equiv_isup_symm_inclusion_apply
equiv_lift 📖	CompOp	1 math math: equiv_lift_of
instStructureDirectLimit 📖	CompOp	17 math math: of_f, lift_unique, liftInclusion_of, cg, Equiv_isup_symm_inclusion, lift_quotient_mk'_sigma_mk', lift_of, of_apply, FirstOrder.Language.age_directLimit, equiv_lift_of, Equiv_isup_of_apply, iSup_range_of_eq_top, Equiv_isup_symm_inclusion_apply, cg', exists_of, range_lift, rangeLiftInclusion
liftInclusion 📖	CompOp	2 math math: liftInclusion_of, rangeLiftInclusion
of 📖	CompOp	12 math math: of_f, lift_unique, liftInclusion_of, exists_fg_substructure_in_Sigma, Equiv_isup_symm_inclusion, lift_of, of_apply, equiv_lift_of, Equiv_isup_of_apply, iSup_range_of_eq_top, Equiv_isup_symm_inclusion_apply, exists_of
prestructure 📖	CompOp	2 math math: funMap_quotient_mk'_sigma_mk', relMap_quotient_mk'_sigma_mk'
setoid 📖	CompOp	8 math math: funMap_quotient_mk'_sigma_mk', exists_quotient_mk'_sigma_mk'_eq, funMap_equiv_unify, relMap_quotient_mk'_sigma_mk', equiv_iff, lift_quotient_mk'_sigma_mk', of_apply, funMap_unify_equiv
sigmaStructure 📖	CompOp	2 math math: funMap_equiv_unify, relMap_equiv_unify
unify 📖	CompOp	7 math math: unify_sigma_mk_self, exists_unify_eq, funMap_equiv_unify, relMap_unify_equiv, relMap_equiv_unify, comp_unify, funMap_unify_equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Equiv_isup_of_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.DirectLimit FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike OrderHom PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder OrderHom.instFunLike FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.inclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice instStructureDirectLimit EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike Equiv_iSup FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike of CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup le_iSup	—	OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion
Equiv_isup_symm_inclusion 📖	mathematical	—	FirstOrder.Language.Embedding.comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe OrderHom PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder OrderHom.instFunLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.DirectLimit FirstOrder.Language.Substructure.inclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion instStructureDirectLimit FirstOrder.Language.Equiv.toEmbedding FirstOrder.Language.Equiv.symm Equiv_iSup le_iSup of	—	FirstOrder.Language.Embedding.ext OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion le_iSup Equiv_isup_symm_inclusion_apply
Equiv_isup_symm_inclusion_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice OrderHom PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder OrderHom.instFunLike FirstOrder.Language.DirectLimit FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.inclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion instStructureDirectLimit EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike FirstOrder.Language.Equiv.symm Equiv_iSup FirstOrder.Language.Embedding CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup FirstOrder.Language.Embedding.funLike le_iSup of	—	FirstOrder.Language.Equiv.injective OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion le_iSup FirstOrder.Language.Equiv.apply_symm_apply
cg 📖	mathematical	FirstOrder.Language.Structure.CG	FirstOrder.Language.DirectLimit instStructureDirectLimit	—	FirstOrder.Language.Structure.CG.out Set.countable_iUnion Set.Countable.image eq_top_iff FirstOrder.Language.Substructure.closure_iUnion Set.image_congr FirstOrder.Language.Substructure.closure_image le_iSup_iff Sigma.eta Quotient.out_eq
cg' 📖	mathematical	FirstOrder.Language.Structure.CG	FirstOrder.Language.DirectLimit instStructureDirectLimit	—	cg
comp_unify 📖	mathematical	Preorder.toLE Set Set.instMembership upperBounds Set.range	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike unify trans instIsTransLe mem_upperBounds	—	trans instIsTransLe mem_upperBounds LE.le.trans FirstOrder.Language.DirectedSystem.map_map
equiv_iff 📖	mathematical	Preorder.toLE	FirstOrder.Language.Structure.Sigma setoid DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike	—	directed_of FirstOrder.Language.Embedding.injective LE.le.trans FirstOrder.Language.DirectedSystem.map_map
equiv_lift_of 📖	mathematical	DFunLike.coe FirstOrder.Language.Equiv EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike	FirstOrder.Language.DirectLimit instStructureDirectLimit equiv_lift of	—	—
exists_fg_substructure_in_Sigma 📖	mathematical	FirstOrder.Language.Substructure.FG FirstOrder.Language.DirectLimit instStructureDirectLimit	FirstOrder.Language.Substructure.map FirstOrder.Language.Embedding.toHom of	—	exists_quotient_mk'_sigma_mk'_eq Finite.of_fintype FirstOrder.Language.Substructure.map_closure Set.image_congr Set.image_univ Set.image_image Subtype.range_coe_subtype Finset.setOf_mem
exists_of 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.funLike of	—	Sigma.eta Quotient.out_eq
exists_quotient_mk'_sigma_mk'_eq 📖	mathematical	—	FirstOrder.Language.Structure.Sigma setoid	—	Finite.bddAbove_range Quotient.eq_mk_iff_out unify.eq_1 le_rfl equiv_iff FirstOrder.Language.DirectedSystem.map_self
exists_unify_eq 📖	mathematical	piSetoid FirstOrder.Language.Structure.Sigma setoid	unify	—	Finite.bddAbove_range Finite.instSum upperBounds_union Set.Sum.elim_range equiv_iff
funMap_equiv_unify 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE Set.range	FirstOrder.Language.Structure.Sigma setoid FirstOrder.Language.Structure.funMap sigmaStructure unify	—	funMap_unify_equiv Finite.bddAbove_range Finite.of_fintype
funMap_quotient_mk'_sigma_mk' 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.Structure.Sigma setoid FirstOrder.Language.quotientStructure prestructure	—	FirstOrder.Language.funMap_quotient_mk' Finite.bddAbove_range Finite.of_fintype directed_of trans instIsTransLe mem_upperBounds FirstOrder.Language.Embedding.map_fun comp_unify
funMap_unify_equiv 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE Set.range	FirstOrder.Language.Structure.Sigma setoid FirstOrder.Language.Structure.funMap unify	—	directed_of FirstOrder.Language.Embedding.map_fun trans instIsTransLe mem_upperBounds comp_unify
iSup_range_of_eq_top 📖	mathematical	—	iSup FirstOrder.Language.Substructure FirstOrder.Language.DirectLimit instStructureDirectLimit ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice FirstOrder.Language.Hom.range FirstOrder.Language.Embedding.toHom of Top.top FirstOrder.Language.Substructure.instTop	—	eq_top_iff inductionOn le_iSup Set.mem_range_self
inductionOn 📖	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.funLike of	—	—	exists_of
liftInclusion_of 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike OrderHom PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder OrderHom.instFunLike FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.inclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion instStructureDirectLimit FirstOrder.Language.Embedding.funLike liftInclusion of FirstOrder.Language.Substructure.subtype	—	OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion
lift_of 📖	mathematical	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike	FirstOrder.Language.DirectLimit instStructureDirectLimit lift of	—	lift_quotient_mk'_sigma_mk'
lift_quotient_mk'_sigma_mk' 📖	mathematical	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike	FirstOrder.Language.DirectLimit instStructureDirectLimit lift FirstOrder.Language.Structure.Sigma setoid	—	—
lift_unique 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.funLike lift FirstOrder.Language.Embedding.comp of	—	inductionOn lift_of
of_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.funLike of FirstOrder.Language.Structure.Sigma setoid	—	—
of_f 📖	mathematical	Preorder.toLE	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.funLike of	—	of_apply Quotient.eq refl instReflLe FirstOrder.Language.DirectedSystem.map_self
rangeLiftInclusion 📖	mathematical	—	FirstOrder.Language.Hom.range FirstOrder.Language.DirectLimit FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe OrderHom PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder OrderHom.instFunLike FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.inclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion instStructureDirectLimit FirstOrder.Language.Embedding.toHom liftInclusion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice	—	OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion range_lift FirstOrder.Language.Substructure.range_subtype
range_lift 📖	mathematical	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike	FirstOrder.Language.Hom.range FirstOrder.Language.DirectLimit instStructureDirectLimit FirstOrder.Language.Embedding.toHom lift iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice	—	FirstOrder.Language.Hom.range_eq_map iSup_range_of_eq_top FirstOrder.Language.Substructure.map_iSup FirstOrder.Language.Substructure.map_map
relMap_equiv_unify 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE Set.range	FirstOrder.Language.Structure.RelMap FirstOrder.Language.Structure.Sigma sigmaStructure unify	—	relMap_unify_equiv Finite.bddAbove_range Finite.of_fintype
relMap_quotient_mk'_sigma_mk' 📖	mathematical	—	FirstOrder.Language.Structure.RelMap FirstOrder.Language.Structure.Sigma setoid FirstOrder.Language.quotientStructure prestructure	—	FirstOrder.Language.relMap_quotient_mk' le_of_eq relMap_equiv_unify trans instIsTransLe refl instReflLe unify_sigma_mk_self
relMap_unify_equiv 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE Set.range	FirstOrder.Language.Structure.RelMap unify	—	directed_of FirstOrder.Language.Embedding.map_rel trans instIsTransLe mem_upperBounds comp_unify
unify_sigma_mk_self 📖	mathematical	—	unify Preorder.toLE trans instIsTransLe le_of_eq refl instReflLe	—	trans instIsTransLe le_of_eq refl instReflLe unify.eq_1 FirstOrder.Language.DirectedSystem.map_self

FirstOrder.Language.DirectedSystem

Definitions

Name	Category	Theorems
natLERec 📖	CompOp	2 math math: coe_natLERec, natLERec.directedSystem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_natLERec 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike natLERec Nat.leRecOn	—	Nat.leRecOn_self le_self_add Nat.instCanonicallyOrderedAdd Nat.leRecOn_succ natLERec.eq_1 FirstOrder.Language.Embedding.comp_apply
map_map 📖	mathematical	Preorder.toLE	DFunLike.coe LE.le.trans	—	DirectedSystem.map_map'
map_self 📖	mathematical	—	DFunLike.coe le_rfl	—	DirectedSystem.map_self'

FirstOrder.Language.DirectedSystem.natLERec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
directedSystem 📖	mathematical	—	DirectedSystem Nat.instPreorder DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike FirstOrder.Language.DirectedSystem.natLERec	—	Nat.leRecOn_self LE.le.trans FirstOrder.Language.DirectedSystem.coe_natLERec Nat.leRecOn_trans

FirstOrder.Language.Structure.Sigma

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Module

Definitions

Name	Category	Theorems
DirectLimit 📖	CompOp	31 math math: DirectLimit.lift_injective, DirectLimit.map_apply_of, ModuleCat.directLimitCocone_pt_carrier, DirectLimit.lift_of, TensorProduct.directLimitRight_tmul_of, DirectLimit.quotMk_of, DirectLimit.congr_symm_apply_of, DirectLimit.map_comp, DirectLimit.of_f, ModuleCat.directLimitIsColimit_desc, Submodule.FG.lTensor.directLimit_apply', DirectLimit.linearEquiv_of, Submodule.FG.rTensor.directLimit_apply, TensorProduct.directLimitLeft_rTensor_of, DirectLimit.lift_comp_of, DirectLimit.congr_apply_of, DirectLimit.exists_of, DirectLimit.map_id, DirectLimit.linearEquiv_symm_mk, DirectLimit.lift_of', Submodule.FG.lTensor.directLimit_apply, fgSystem.equiv_comp_of, ModuleCat.directLimitCocone_ι_app, TensorProduct.directLimitLeft_tmul_of, TensorProduct.directLimitLeft_symm_of_tmul, TensorProduct.fromDirectLimit_of_tmul, TensorProduct.directLimitRight_symm_of_tmul, Submodule.FG.rTensor.directLimit_apply', DirectLimit.hom_ext_iff, DirectLimit.exists_of₂, TensorProduct.toDirectLimit_tmul_of

Ring

Definitions

Name	Category	Theorems
DirectLimit 📖	CompOp	21 math math: DirectLimit.congr_symm_apply_of, Field.DirectLimit.exists_inv, Field.DirectLimit.nontrivial, DirectLimit.congr_apply_of, DirectLimit.of_injective, Field.DirectLimit.mul_inv_cancel, DirectLimit.hom_ext_iff, DirectLimit.ringEquiv_of, DirectLimit.quotientMk_of, DirectLimit.map_id, DirectLimit.map_comp, DirectLimit.lift_comp_of, DirectLimit.ringEquiv_symm_mk, Field.DirectLimit.inv_mul_cancel, DirectLimit.lift_of, DirectLimit.exists_of, DirectLimit.Polynomial.exists_of, DirectLimit.lift_injective, DirectLimit.map_apply_of, DirectLimit.of_f, DirectLimit.lift_of'

(root)

Definitions

Name	Category	Theorems
DirectLimit 📖	CompOp	21 math math: DirectLimit.Module.of_f, DirectLimit.Module.lift_of, DirectLimit.ratCast_def, DirectLimit.instNontrivial, DirectLimit.natCast_def, Module.DirectLimit.linearEquiv_of, DirectLimit.exists_eq_one, DirectLimit.intCast_def, Module.DirectLimit.linearEquiv_symm_mk, DirectLimit.Ring.of_f, Ring.DirectLimit.ringEquiv_of, DirectLimit.exists_eq_zero, DirectLimit.one_def, DirectLimit.Ring.hom_ext_iff, DirectLimit.Ring.lift_of, Ring.DirectLimit.ringEquiv_symm_mk, DirectLimit.Module.hom_ext_iff, DirectLimit.Module.lift_apply, DirectLimit.zero_def, DirectLimit.nnratCast_def, DirectLimit.lift_injective

---

← Back to Index