PartialEquiv

📁 Source: Mathlib/ModelTheory/PartialEquiv.lean

Statistics

Metric	Count
Definitions partialEquivLimit, toPartialEquiv, FGEquiv, IsExtensionPair, definedAtLeft, definedAtRight, PartialEquiv, cod, codRestrict, dom, domRestrict, instInhabited_self, instLE, instPartialOrder, toEmbedding, toEmbeddingOfEqTop, toEquiv, toEquivOfEqTop, inhabited_FGEquiv_of_IsEmpty_Constants_and_Relations, inhabited_self_FGEquiv, «term_≃ₚ[_]_», PartialEquiv	22
Theorems cod_partialEquivLimit, dom_partialEquivLimit, instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, le_partialEquivLimit, partialEquivLimit_comp_inclusion, toEmbedding_toPartialEquiv, toPartialEquiv_injective, toPartialEquiv_toEmbedding, symm_coe, cod, codRestrict_le, cod_le_cod, domRestrict_le, dom_fg_iff_cod_fg, dom_le_dom, ext, ext_iff, le_codRestrict, le_def, le_domRestrict, le_iff, le_trans, monotone_cod, monotone_dom, monotone_symm, subtype_toEquiv_inclusion, symm_apply, symm_bijective, symm_le_iff, symm_le_symm, symm_symm, toEmbeddingOfEqTop_apply, toEmbedding_apply, toEquivOfEqTop_toEmbedding, toEquiv_inclusion, toEquiv_inclusion_apply, countable_self_fgequiv_of_countable, embedding_from_cg, equiv_between_cg, isExtensionPair_iff_cod, isExtensionPair_iff_exists_embedding_closure_singleton_sup	42
Total	64

FirstOrder

Definitions

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

FirstOrder.Language

Definitions

Name	Category	Theorems
FGEquiv 📖	CompOp	3 math math: IsExtensionPair.cod, isExtensionPair_iff_cod, countable_self_fgequiv_of_countable
IsExtensionPair 📖	MathDef	5 math math: dlo_isExtensionPair, isExtensionPair_iff_cod, isExtensionPair_iff_exists_embedding_closure_singleton_sup, IsFraisseLimit.isExtensionPair, isUltrahomogeneous_iff_IsExtensionPair
PartialEquiv 📖	CompData	21 math math: IsExtensionPair.cod, PartialEquiv.monotone_symm, PartialEquiv.codRestrict_le, embedding_from_cg, DirectLimit.partialEquivLimit_comp_inclusion, PartialEquiv.domRestrict_le, PartialEquiv.le_iff, Embedding.toPartialEquiv_injective, PartialEquiv.symm_bijective, isExtensionPair_iff_cod, PartialEquiv.symm_le_iff, PartialEquiv.monotone_cod, PartialEquiv.le_def, equiv_between_cg, DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, PartialEquiv.monotone_dom, DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, FGEquiv.symm_coe, DirectLimit.cod_partialEquivLimit, DirectLimit.le_partialEquivLimit, DirectLimit.dom_partialEquivLimit
inhabited_FGEquiv_of_IsEmpty_Constants_and_Relations 📖	CompOp	—
inhabited_self_FGEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countable_self_fgequiv_of_countable 📖	mathematical	—	Countable FGEquiv	—	Subtype.prop PartialEquiv.ext Substructure.fg_iff_structure_fg Function.Embedding.countable instCountableSigma Substructure.instCountable_fg_substructures_of_countable Structure.FG.instCountable_hom
embedding_from_cg 📖	mathematical	IsExtensionPair	PartialEquiv PartialEquiv.instLE Substructure.FG PartialEquiv.dom Embedding.toPartialEquiv	—	Monotone.comp Subtype.mono_coe Order.sequenceOfCofinals.monotone SemilatticeSup.instIsDirectedOrder Order.sequenceOfCofinals.encode_mem PartialEquiv.dom_le_dom DirectLimit.le_partialEquivLimit top_le_iff Substructure.closure_le Embedding.toPartialEquiv_toEmbedding
equiv_between_cg 📖	mathematical	IsExtensionPair	PartialEquiv PartialEquiv.instLE Substructure.FG PartialEquiv.dom Embedding.toPartialEquiv Equiv.toEmbedding	—	Monotone.comp Subtype.mono_coe Order.sequenceOfCofinals.monotone SemilatticeSup.instIsDirectedOrder Order.sequenceOfCofinals.encode_mem PartialEquiv.dom_le_dom DirectLimit.le_partialEquivLimit PartialEquiv.cod_le_cod top_le_iff Substructure.closure_le PartialEquiv.toEquivOfEqTop_toEmbedding Embedding.toPartialEquiv_toEmbedding
isExtensionPair_iff_cod 📖	mathematical	—	IsExtensionPair Substructure SetLike.instMembership Substructure.instSetLike PartialEquiv.cod PartialEquiv Substructure.FG PartialEquiv.dom FGEquiv PartialEquiv.instLE	—	PartialEquiv.monotone_symm
isExtensionPair_iff_exists_embedding_closure_singleton_sup 📖	mathematical	—	IsExtensionPair Embedding.comp Substructure SetLike.instMembership Substructure.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Substructure.instCompleteLattice LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Substructure.instPartialOrder SetLike.coe Substructure.closure Set.instSingletonSet Substructure.inducedStructure Substructure.inclusion le_sup_right	—	le_sup_right Embedding.ext Embedding.subtype_equivRange Substructure.FG.sup Substructure.fg_closure_singleton HasSubset.Subset.trans Set.instIsTransSubset Substructure.subset_closure le_sup_left Set.mem_singleton PartialEquiv.toEmbedding.eq_1

FirstOrder.Language.DirectLimit

Definitions

Name	Category	Theorems
partialEquivLimit 📖	CompOp	4 math math: partialEquivLimit_comp_inclusion, cod_partialEquivLimit, le_partialEquivLimit, dom_partialEquivLimit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cod_partialEquivLimit 📖	mathematical	—	FirstOrder.Language.PartialEquiv.cod partialEquivLimit iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice DFunLike.coe OrderHom FirstOrder.Language.PartialEquiv PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike	—	—
dom_partialEquivLimit 📖	mathematical	—	FirstOrder.Language.PartialEquiv.dom partialEquivLimit iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice FirstOrder.Language.Substructure.instCompleteLattice DFunLike.coe OrderHom FirstOrder.Language.PartialEquiv PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike	—	—
instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion 📖	mathematical	—	DirectedSystem FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.PartialEquiv.cod DFunLike.coe OrderHom FirstOrder.Language.PartialEquiv PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike FirstOrder.Language.Embedding FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.inclusion FirstOrder.Language.PartialEquiv.cod_le_cod OrderHom.monotone	—	FirstOrder.Language.PartialEquiv.cod_le_cod OrderHom.monotone le_rfl
instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion 📖	mathematical	—	DirectedSystem FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.PartialEquiv.dom DFunLike.coe OrderHom FirstOrder.Language.PartialEquiv PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike FirstOrder.Language.Embedding FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.inclusion FirstOrder.Language.PartialEquiv.dom_le_dom OrderHom.monotone	—	FirstOrder.Language.PartialEquiv.dom_le_dom OrderHom.monotone le_rfl
le_partialEquivLimit 📖	mathematical	—	FirstOrder.Language.PartialEquiv FirstOrder.Language.PartialEquiv.instLE DFunLike.coe OrderHom PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike partialEquivLimit	—	le_iSup partialEquivLimit_comp_inclusion
partialEquivLimit_comp_inclusion 📖	mathematical	—	FirstOrder.Language.Embedding.comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.PartialEquiv.dom DFunLike.coe OrderHom FirstOrder.Language.PartialEquiv PartialOrder.toPreorder FirstOrder.Language.PartialEquiv.instPartialOrder OrderHom.instFunLike partialEquivLimit FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.PartialEquiv.cod FirstOrder.Language.Equiv.toEmbedding FirstOrder.Language.PartialEquiv.toEquiv FirstOrder.Language.Substructure.inclusion le_iSup FirstOrder.Language.Substructure.instCompleteLattice iSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	le_iSup instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion OrderHom.monotone FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion Equiv_isup_symm_inclusion

FirstOrder.Language.Embedding

Definitions

Name	Category	Theorems
toPartialEquiv 📖	CompOp	5 math math: toPartialEquiv_toEmbedding, FirstOrder.Language.embedding_from_cg, toPartialEquiv_injective, toEmbedding_toPartialEquiv, FirstOrder.Language.equiv_between_cg

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toEmbedding_toPartialEquiv 📖	mathematical	—	FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop toPartialEquiv FirstOrder.Language.Substructure FirstOrder.Language.PartialEquiv.dom	—	—
toPartialEquiv_injective 📖	mathematical	—	FirstOrder.Language.Embedding FirstOrder.Language.PartialEquiv toPartialEquiv	—	ext FirstOrder.Language.PartialEquiv.ext_iff FirstOrder.Language.Substructure.mem_top
toPartialEquiv_toEmbedding 📖	mathematical	FirstOrder.Language.PartialEquiv.dom Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop	toPartialEquiv FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop	—	FirstOrder.Language.PartialEquiv.ext

FirstOrder.Language.FGEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
symm_coe 📖	mathematical	—	FirstOrder.Language.PartialEquiv FirstOrder.Language.Substructure.FG FirstOrder.Language.PartialEquiv.dom symm FirstOrder.Language.PartialEquiv.symm	—	—

FirstOrder.Language.IsExtensionPair

Definitions

Name	Category	Theorems
definedAtLeft 📖	CompOp	—
definedAtRight 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cod 📖	mathematical	FirstOrder.Language.IsExtensionPair	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.PartialEquiv.cod FirstOrder.Language.PartialEquiv FirstOrder.Language.Substructure.FG FirstOrder.Language.PartialEquiv.dom FirstOrder.Language.FGEquiv FirstOrder.Language.PartialEquiv.instLE	—	FirstOrder.Language.isExtensionPair_iff_cod

FirstOrder.Language.PartialEquiv

Definitions

Name	Category	Theorems
cod 📖	CompOp	17 math math: toEmbedding_apply, FirstOrder.Language.IsExtensionPair.cod, dom_fg_iff_cod_fg, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, le_iff, subtype_toEquiv_inclusion, FirstOrder.Language.isExtensionPair_iff_cod, monotone_cod, toEquiv_inclusion_apply, le_def, cod_le_cod, symm_apply, toEmbeddingOfEqTop_apply, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, ext_iff, toEquiv_inclusion
codRestrict 📖	CompOp	2 math math: codRestrict_le, le_codRestrict
dom 📖	CompOp	20 math math: toEmbedding_apply, FirstOrder.Language.IsExtensionPair.cod, dom_fg_iff_cod_fg, dom_le_dom, FirstOrder.Language.embedding_from_cg, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, le_iff, FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv, subtype_toEquiv_inclusion, FirstOrder.Language.isExtensionPair_iff_cod, toEquiv_inclusion_apply, le_def, FirstOrder.Language.equiv_between_cg, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, monotone_dom, symm_apply, FirstOrder.Language.FGEquiv.symm_coe, ext_iff, toEquiv_inclusion, FirstOrder.Language.DirectLimit.dom_partialEquivLimit
domRestrict 📖	CompOp	2 math math: le_domRestrict, domRestrict_le
instInhabited_self 📖	CompOp	—
instLE 📖	CompOp	10 math math: FirstOrder.Language.IsExtensionPair.cod, codRestrict_le, FirstOrder.Language.embedding_from_cg, domRestrict_le, le_iff, FirstOrder.Language.isExtensionPair_iff_cod, symm_le_iff, le_def, FirstOrder.Language.equiv_between_cg, FirstOrder.Language.DirectLimit.le_partialEquivLimit
instPartialOrder 📖	CompOp	9 math math: monotone_symm, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, monotone_cod, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, monotone_dom, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, FirstOrder.Language.DirectLimit.le_partialEquivLimit, FirstOrder.Language.DirectLimit.dom_partialEquivLimit
toEmbedding 📖	CompOp	1 math math: toEmbedding_apply
toEmbeddingOfEqTop 📖	CompOp	4 math math: FirstOrder.Language.Embedding.toPartialEquiv_toEmbedding, FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv, toEquivOfEqTop_toEmbedding, toEmbeddingOfEqTop_apply
toEquiv 📖	CompOp	10 math math: toEmbedding_apply, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, le_iff, subtype_toEquiv_inclusion, toEquiv_inclusion_apply, le_def, symm_apply, toEmbeddingOfEqTop_apply, ext_iff, toEquiv_inclusion
toEquivOfEqTop 📖	CompOp	1 math math: toEquivOfEqTop_toEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict_le 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder cod	FirstOrder.Language.PartialEquiv instLE codRestrict	—	symm_le_iff domRestrict_le
cod_le_cod 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder cod	—	FirstOrder.Language.Equiv.apply_symm_apply
domRestrict_le 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder dom	FirstOrder.Language.PartialEquiv instLE domRestrict	—	—
dom_fg_iff_cod_fg 📖	mathematical	—	FirstOrder.Language.Substructure.FG dom cod	—	FirstOrder.Language.Substructure.fg_iff_structure_fg FirstOrder.Language.Equiv.fg_iff
dom_le_dom 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder dom	—	—
ext 📖	—	dom DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike cod FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv	—	—	le_def le_rfl FirstOrder.Language.Embedding.ext
ext_iff 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike cod FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv dom EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv	—	ext
le_codRestrict 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder cod FirstOrder.Language.PartialEquiv instLE	codRestrict	—	symm_le_iff le_domRestrict monotone_symm
le_def 📖	mathematical	—	FirstOrder.Language.PartialEquiv instLE FirstOrder.Language.Embedding.comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom cod FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv.toEmbedding toEquiv FirstOrder.Language.Substructure.inclusion	—	—
le_domRestrict 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder dom FirstOrder.Language.PartialEquiv instLE	domRestrict	—	dom_le_dom subtype_toEquiv_inclusion
le_iff 📖	mathematical	—	FirstOrder.Language.PartialEquiv instLE DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike cod FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.inclusion FirstOrder.Language.Equiv dom EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv	—	dom_le_dom cod_le_cod Function.Embedding.inj' toEquiv_inclusion_apply le_def FirstOrder.Language.Embedding.ext
le_trans 📖	—	FirstOrder.Language.PartialEquiv instLE	—	—	LE.le.trans FirstOrder.Language.Embedding.comp_assoc FirstOrder.Language.Embedding.ext
monotone_cod 📖	mathematical	—	Monotone FirstOrder.Language.PartialEquiv FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder FirstOrder.Language.Substructure.instPartialOrder cod	—	cod_le_cod
monotone_dom 📖	mathematical	—	Monotone FirstOrder.Language.PartialEquiv FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder FirstOrder.Language.Substructure.instPartialOrder dom	—	dom_le_dom
monotone_symm 📖	mathematical	—	Monotone FirstOrder.Language.PartialEquiv PartialOrder.toPreorder instPartialOrder symm	—	symm_le_symm
subtype_toEquiv_inclusion 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	FirstOrder.Language.Embedding.comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom cod FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv.toEmbedding toEquiv FirstOrder.Language.Substructure.inclusion dom_le_dom	—	dom_le_dom
symm_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom symm cod FirstOrder.Language.Substructure.inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv FirstOrder.Language.Equiv.symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective FirstOrder.Language.PartialEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_le_iff 📖	mathematical	—	FirstOrder.Language.PartialEquiv instLE symm	—	symm_symm monotone_symm
symm_le_symm 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	symm	—	le_iff cod_le_cod dom_le_dom FirstOrder.Language.Equiv.injective FirstOrder.Language.Equiv.apply_symm_apply FirstOrder.Language.Equiv.symm_apply_apply toEquiv_inclusion_apply
symm_symm 📖	mathematical	—	symm	—	—
toEmbeddingOfEqTop_apply 📖	mathematical	dom Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike toEmbeddingOfEqTop SetLike.instMembership FirstOrder.Language.Substructure.instSetLike cod FirstOrder.Language.Equiv FirstOrder.Language.Substructure.inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv FirstOrder.Language.Substructure.mem_top	—	FirstOrder.Language.Substructure.mem_top
toEmbedding_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.funLike toEmbedding cod FirstOrder.Language.Equiv EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv	—	—
toEquivOfEqTop_toEmbedding 📖	mathematical	dom Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop cod	FirstOrder.Language.Equiv.toEmbedding toEquivOfEqTop toEmbeddingOfEqTop	—	—
toEquiv_inclusion 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	FirstOrder.Language.Embedding.comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom FirstOrder.Language.Substructure.inducedStructure cod FirstOrder.Language.Equiv.toEmbedding toEquiv FirstOrder.Language.Substructure.inclusion dom_le_dom cod_le_cod	—	dom_le_dom cod_le_cod subtype_toEquiv_inclusion FirstOrder.Language.Embedding.ext
toEquiv_inclusion_apply 📖	mathematical	FirstOrder.Language.PartialEquiv instLE	DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike dom cod FirstOrder.Language.Substructure.inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike toEquiv FirstOrder.Language.Embedding FirstOrder.Language.Embedding.funLike FirstOrder.Language.Substructure.inclusion dom_le_dom cod_le_cod	—	FirstOrder.Language.Embedding.injective dom_le_dom cod_le_cod subtype_toEquiv_inclusion

(root)

Definitions

Name	Category	Theorems
PartialEquiv 📖	CompData	9 math math: Pretrivialization.toPartialEquiv_injective, PartialEquiv.symm_trans_self, OpenPartialHomeomorph.toPartialEquiv_injective, ChartedSpaceCore.chart_mem_atlas, PartialEquiv.symm_bijective, Equidecomp.toPartialEquiv_injective, PartialEquiv.eqOnSource_refl, PartialEquiv.self_trans_symm, FiberBundleCore.localTrivAsPartialEquiv_trans

---

← Back to Index