Substructures

📁 Source: Mathlib/ModelTheory/Substructures.lean

Statistics

Metric	Count
Definitions ClosedUnder, codRestrict, domRestrict, equivRange, substructureEquivMap, codRestrict, domRestrict, eqLocus, range, substructureReduct, Substructure, carrier, closure, comap, copy, gciMapComap, gi, giMapComap, inclusion, inducedStructure, instCompleteLattice, instInf, instInfSet, instInhabited, instPartialOrder, instSetLike, instTop, map, subtype, topEquiv, withConstants	31
Theorems inf, inter, sInf, codRestrict_apply, codRestrict_apply', comp_codRestrict, domRestrict_apply, equivRange_apply, equivRange_toEquiv_apply, substructureEquivMap_apply, subtype_comp_codRestrict, subtype_equivRange, subtype_substructureEquivMap, toHom_range, codRestrict_toFun_coe, comp_codRestrict, domRestrict_toFun, eqOn_closure, eq_of_eqOn_dense, eq_of_eqOn_top, map_le_range, mem_eqLocus, mem_range, mem_range_self, range_coe, range_comp, range_comp_le_range, range_eq_map, range_eq_top, range_id, range_le_iff_comap, subtype_comp_codRestrict, coe_substructureReduct, mem_substructureReduct, apply_coe_mem_map, closed, closure_empty, closure_eq, closure_eq_of_isRelational, closure_eq_of_le, closure_iUnion, closure_image, closure_induction, closure_induction', closure_insert, closure_le, closure_mono, closure_union, closure_univ, closure_withConstants_eq, coe_closure_eq_range_term_realize, coe_comap, coe_copy, coe_iInf, coe_inclusion, coe_inf, coe_map, coe_sInf, coe_subtype, coe_top, coe_topEquiv, coe_withConstants, comap_comap, comap_iInf, comap_iInf_map_of_injective, comap_iSup_map_of_injective, comap_id, comap_inf, comap_inf_map_of_injective, comap_injective_of_surjective, comap_le_comap_iff_of_surjective, comap_map_comap, comap_map_eq_of_injective, comap_strictMono_of_surjective, comap_sup_map_of_injective, comap_surjective_of_injective, comap_top, constants_mem, copy_eq, dense_induction, ext, ext_iff, fun_mem, gc_map_comap, iSup_eq_closure, inclusion_self, instIsEmptySubtypeMemBotOfConstants, le_comap_map, le_comap_of_map_le, lift_card_closure_le, lift_card_closure_le_card_term, map_bot, map_closure, map_comap_eq_of_surjective, map_comap_le, map_comap_map, map_iInf_comap_of_surjective, map_iSup, map_iSup_comap_of_surjective, map_id, map_inf_comap_of_surjective, map_injective_of_injective, map_le_iff_le_comap, map_le_map_iff_of_injective, map_le_of_le_comap, map_map, map_strictMono_of_injective, map_sup, map_sup_comap_of_surjective, map_surjective_of_surjective, mem_carrier, mem_closed_iff, mem_closed_of_isRelational, mem_closure, mem_closure_iff_exists_term, mem_closure_iff_of_isRelational, mem_comap, mem_iInf, mem_iSup_of_directed, mem_inf, mem_map, mem_map_of_mem, mem_sInf, mem_sSup_of_directedOn, mem_top, mem_withConstants, monotone_comap, monotone_map, notMem_of_notMem_closure, range_subtype, realize_boundedFormula_top, realize_formula_top, reduct_withConstants, small_bot, small_closure, subset_closure, subset_closure_withConstants, subtype_apply, subtype_comp_inclusion, subtype_injective, realize_mem, closedUnder_univ, substructure_closure	143
Total	174

FirstOrder.Language

Definitions

Name	Category	Theorems
ClosedUnder 📖	MathDef	3 math math: Substructure.fun_mem, closedUnder_univ, Substructure.mem_closed_iff
Substructure 📖	CompData	163 math math: PartialEquiv.toEmbedding_apply, Substructure.closure_eq_of_isRelational, IsExtensionPair.cod, Substructure.gc_map_comap, Structure.fg_def, Embedding.equivRange_toEquiv_apply, Substructure.map_iInf_comap_of_surjective, Substructure.comap_inf_map_of_injective, Substructure.fg_closure_singleton, Substructure.map_sup, Substructure.comap_strictMono_of_surjective, Substructure.ext_iff, PartialEquiv.dom_le_dom, Hom.range_le_iff_comap, Substructure.small_closure, Substructure.coe_inf, Substructure.cg_def, Substructure.mem_closure, Hom.domRestrict_toFun, Substructure.mem_inf, Substructure.fg_closure, Substructure.map_sup_comap_of_surjective, Substructure.coe_comap, Substructure.subtype_apply, Substructure.comap_sup_map_of_injective, Substructure.inclusion_self, Substructure.small_bot, Substructure.constants_mem, Hom.mem_range, instOrderedStructureSubtypeMemSubstructure, Hom.mem_range_self, Substructure.fg_iff_structure_fg, Substructure.comap_surjective_of_injective, Substructure.coe_subtype, Substructure.cg_bot, Substructure.cg_iff_structure_cg, Substructure.fg_def, Substructure.coe_sInf, Substructure.lift_card_closure_le_card_term, DirectLimit.partialEquivLimit_comp_inclusion, LHom.coe_substructureReduct, Substructure.mem_closure_iff_exists_term, PartialEquiv.le_iff, Substructure.realize_formula_top, Embedding.subtype_equivRange, Substructure.map_comap_le, realize_term_substructure, Embedding.toEmbedding_toPartialEquiv, Substructure.coe_top, Substructure.skolem₁_reduct_isElementary, DirectLimit.liftInclusion_of, PartialEquiv.subtype_toEquiv_inclusion, Substructure.range_subtype, isExtensionPair_iff_cod, Hom.range_eq_map, Embedding.substructureEquivMap_apply, Substructure.mem_closed_of_isRelational, Substructure.fg_iff_exists_fin_generating_family, isExtensionPair_iff_exists_embedding_closure_singleton_sup, Substructure.closure_insert, age.fg_substructure, Substructure.CG.sup, PartialEquiv.monotone_cod, Substructure.closure_empty, PartialEquiv.toEquiv_inclusion_apply, Substructure.iSup_eq_closure, Hom.mem_eqLocus, Substructure.map_bot, Substructure.coe_map, Substructure.monotone_map, Structure.cg_def, DirectLimit.Equiv_isup_symm_inclusion, Substructure.subset_closure, Substructure.closure_iUnion, Substructure.subtype_injective, Hom.range_id, Substructure.map_injective_of_injective, Substructure.closure_union, Substructure.comap_iSup_map_of_injective, Structure.cg_iff, Substructure.FG.sup, Substructure.comap_injective_of_surjective, PartialEquiv.le_def, Substructure.FG.finite, Equiv.toHom_range, Substructure.map_iSup_comap_of_surjective, age.has_representative_as_substructure, Substructure.instCountable_fg_substructures_of_countable, PartialEquiv.cod_le_cod, Substructure.comap_inf, Substructure.map_le_iff_le_comap, Substructure.le_comap_map, Hom.range_coe, Substructure.coe_closure_eq_range_term_realize, Substructure.closed, Substructure.coe_topEquiv, Substructure.coeSort_elementarySkolem₁Reduct, Substructure.comap_iInf, Substructure.comap_top, DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, Hom.range_comp_le_range, Substructure.elementarySkolem₁Reduct.instSmall, Hom.range_eq_top, Substructure.mem_carrier, PartialEquiv.monotone_dom, Hom.map_le_range, Substructure.closure_withConstants_eq, PartialEquiv.symm_apply, DirectLimit.Equiv_isup_of_apply, Substructure.mem_iInf, Substructure.comap_iInf_map_of_injective, Substructure.map_closure, Substructure.monotone_comap, instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, Substructure.comap_le_comap_iff_of_surjective, Substructure.closure_le, DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, Substructure.mem_closed_iff, DirectLimit.iSup_range_of_eq_top, Substructure.instIsEmptySubtypeMemBotOfConstants, Set.Countable.substructure_closure, Substructure.subset_closure_withConstants, Substructure.realize_boundedFormula_top, LHom.mem_substructureReduct, Embedding.subtype_substructureEquivMap, Structure.CG.out, Substructure.mem_sInf, DirectLimit.Equiv_isup_symm_inclusion_apply, Substructure.cg_iff_empty_or_exists_nat_generating_family, Substructure.coe_iInf, Substructure.map_iSup, Substructure.map_le_map_iff_of_injective, Substructure.cg_iff_countable, Structure.FG.out, Substructure.map_surjective_of_surjective, Hom.eqOn_closure, Substructure.models_of_isUniversal, Substructure.mem_map, Substructure.mem_comap, Substructure.fg_bot, DirectLimit.cod_partialEquivLimit, DirectLimit.range_lift, Substructure.mem_top, PartialEquiv.ext_iff, PartialEquiv.toEquiv_inclusion, Embedding.domRestrict_apply, Substructure.lift_card_closure_le, Substructure.closure_eq, Embedding.equivRange_apply, Substructure.map_inf_comap_of_surjective, Substructure.mem_closure_iff_of_isRelational, Substructure.closure_mono, Substructure.countable_fg_substructures_of_countable, DirectLimit.rangeLiftInclusion, Substructure.closure_univ, DirectLimit.dom_partialEquivLimit, Substructure.map_strictMono_of_injective, Substructure.closure_image, Substructure.apply_coe_mem_map, Substructure.fg_iff_finite, Substructure.cg_closure_singleton, Structure.fg_iff, Substructure.cg_closure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedUnder_univ 📖	mathematical	—	ClosedUnder Set.univ	—	Set.mem_univ

FirstOrder.Language.ClosedUnder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inf 📖	mathematical	FirstOrder.Language.ClosedUnder	Set SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	inter
inter 📖	mathematical	FirstOrder.Language.ClosedUnder	Set Set.instInter	—	Set.mem_inter Set.mem_of_mem_inter_left Set.mem_of_mem_inter_right
sInf 📖	mathematical	FirstOrder.Language.ClosedUnder	InfSet.sInf Set Set.instInfSet	—	—

FirstOrder.Language.Embedding

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	5 math math: equivRange_toEquiv_apply, comp_codRestrict, subtype_comp_codRestrict, codRestrict_apply, codRestrict_apply'
domRestrict 📖	CompOp	1 math math: domRestrict_apply
equivRange 📖	CompOp	3 math math: equivRange_toEquiv_apply, subtype_equivRange, equivRange_apply
substructureEquivMap 📖	CompOp	2 math math: substructureEquivMap_apply, subtype_substructureEquivMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict_apply 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Embedding funLike	FirstOrder.Language.Substructure.inducedStructure codRestrict	—	—
codRestrict_apply' 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Embedding funLike	FirstOrder.Language.Substructure.inducedStructure codRestrict	—	—
comp_codRestrict 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Embedding funLike	comp FirstOrder.Language.Substructure.inducedStructure codRestrict	—	ext
domRestrict_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.inducedStructure funLike domRestrict	—	—
equivRange_apply 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Hom.range toHom DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure.inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike equivRange FirstOrder.Language.Embedding funLike	—	—
equivRange_toEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Hom.range toHom EquivLike.toFunLike Equiv.instEquivLike FirstOrder.Language.Equiv.toEquiv FirstOrder.Language.Substructure.inducedStructure equivRange FirstOrder.Language.Embedding funLike codRestrict	—	—
substructureEquivMap_apply 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.map toHom DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure.inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike substructureEquivMap FirstOrder.Language.Embedding funLike	—	—
subtype_comp_codRestrict 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Embedding funLike	comp FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.subtype codRestrict	—	ext
subtype_equivRange 📖	mathematical	—	comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Hom.range toHom FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv.toEmbedding equivRange	—	ext
subtype_substructureEquivMap 📖	mathematical	—	comp FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.map toHom FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Substructure.subtype FirstOrder.Language.Equiv.toEmbedding substructureEquivMap	—	ext

FirstOrder.Language.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHom_range 📖	mathematical	—	FirstOrder.Language.Hom.range toHom Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop	—	FirstOrder.Language.Substructure.ext apply_symm_apply

FirstOrder.Language.Hom

Definitions

Name	Category	Theorems
codRestrict 📖	CompOp	3 math math: subtype_comp_codRestrict, comp_codRestrict, codRestrict_toFun_coe
domRestrict 📖	CompOp	1 math math: domRestrict_toFun
eqLocus 📖	CompOp	1 math math: mem_eqLocus
range 📖	CompOp	20 math math: FirstOrder.Language.Embedding.equivRange_toEquiv_apply, range_le_iff_comap, mem_range, mem_range_self, FirstOrder.Language.Embedding.subtype_equivRange, FirstOrder.Language.Substructure.range_subtype, range_eq_map, FirstOrder.Language.Structure.CG.range, range_id, FirstOrder.Language.Equiv.toHom_range, range_coe, range_comp_le_range, range_eq_top, map_le_range, range_comp, FirstOrder.Language.Structure.FG.range, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, FirstOrder.Language.DirectLimit.range_lift, FirstOrder.Language.Embedding.equivRange_apply, FirstOrder.Language.DirectLimit.rangeLiftInclusion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codRestrict_toFun_coe 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Hom instFunLike	FirstOrder.Language.Substructure.inducedStructure codRestrict	—	—
comp_codRestrict 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Hom instFunLike	comp FirstOrder.Language.Substructure.inducedStructure codRestrict	—	ext
domRestrict_toFun 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.inducedStructure instFunLike domRestrict	—	—
eqOn_closure 📖	mathematical	Set.EqOn DFunLike.coe FirstOrder.Language.Hom instFunLike	SetLike.coe FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra FirstOrder.Language.Substructure.instPartialOrder FirstOrder.Language.Substructure.closure	—	FirstOrder.Language.Substructure.closure_le
eq_of_eqOn_dense 📖	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra FirstOrder.Language.Substructure.instPartialOrder SetLike.coe FirstOrder.Language.Substructure.instSetLike FirstOrder.Language.Substructure.closure Top.top FirstOrder.Language.Substructure.instTop Set.EqOn DFunLike.coe FirstOrder.Language.Hom instFunLike	—	—	eq_of_eqOn_top eqOn_closure
eq_of_eqOn_top 📖	—	Set.EqOn DFunLike.coe FirstOrder.Language.Hom instFunLike SetLike.coe FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instSetLike Top.top FirstOrder.Language.Substructure.instTop	—	—	ext
map_le_range 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder FirstOrder.Language.Substructure.map range	—	SetLike.coe_mono instIsConcreteLE Set.image_subset_range
mem_eqLocus 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike eqLocus DFunLike.coe FirstOrder.Language.Hom instFunLike	—	—
mem_range 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike range DFunLike.coe FirstOrder.Language.Hom instFunLike	—	—
mem_range_self 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike range DFunLike.coe FirstOrder.Language.Hom instFunLike	—	—
range_coe 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instSetLike range Set.range DFunLike.coe FirstOrder.Language.Hom instFunLike	—	—
range_comp 📖	mathematical	—	range comp FirstOrder.Language.Substructure.map	—	SetLike.coe_injective Set.range_comp
range_comp_le_range 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder range comp	—	SetLike.coe_mono instIsConcreteLE Set.range_comp_subset_range
range_eq_map 📖	mathematical	—	range FirstOrder.Language.Substructure.map Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop	—	FirstOrder.Language.Substructure.ext
range_eq_top 📖	mathematical	—	range Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop DFunLike.coe FirstOrder.Language.Hom instFunLike	—	SetLike.ext'_iff range_coe FirstOrder.Language.Substructure.coe_top Set.range_eq_univ
range_id 📖	mathematical	—	range id Top.top FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instTop	—	SetLike.coe_injective Set.range_id
range_le_iff_comap 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder range FirstOrder.Language.Substructure.comap Top.top FirstOrder.Language.Substructure.instTop	—	range_eq_map FirstOrder.Language.Substructure.map_le_iff_le_comap eq_top_iff
subtype_comp_codRestrict 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe FirstOrder.Language.Hom instFunLike	comp FirstOrder.Language.Substructure.inducedStructure FirstOrder.Language.Embedding.toHom FirstOrder.Language.Substructure.subtype codRestrict	—	ext

FirstOrder.Language.LHom

Definitions

Name	Category	Theorems
substructureReduct 📖	CompOp	4 math math: coe_substructureReduct, FirstOrder.Language.Substructure.skolem₁_reduct_isElementary, FirstOrder.Language.Substructure.reduct_withConstants, mem_substructureReduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_substructureReduct 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure FirstOrder.Language.Substructure.instSetLike DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder instFunLikeOrderEmbedding substructureReduct	—	—
mem_substructureReduct 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike DFunLike.coe OrderEmbedding Preorder.toLE PartialOrder.toPreorder FirstOrder.Language.Substructure.instPartialOrder instFunLikeOrderEmbedding substructureReduct	—	—

FirstOrder.Language.Substructure

Definitions

Name	Category	Theorems
carrier 📖	CompOp	2 math math: fun_mem, mem_carrier
closure 📖	CompOp	38 math math: closure_eq_of_isRelational, fg_closure_singleton, small_closure, cg_def, mem_closure, fg_closure, fg_def, lift_card_closure_le_card_term, mem_closure_iff_exists_term, mem_closed_of_isRelational, fg_iff_exists_fin_generating_family, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, closure_insert, closure_empty, iSup_eq_closure, subset_closure, closure_iUnion, closure_union, FirstOrder.Language.Structure.cg_iff, coe_closure_eq_range_term_realize, closed, closure_withConstants_eq, map_closure, closure_le, mem_closed_iff, Set.Countable.substructure_closure, subset_closure_withConstants, cg_iff_empty_or_exists_nat_generating_family, FirstOrder.Language.Hom.eqOn_closure, lift_card_closure_le, closure_eq, mem_closure_iff_of_isRelational, closure_mono, closure_univ, closure_image, cg_closure_singleton, FirstOrder.Language.Structure.fg_iff, cg_closure
comap 📖	CompOp	30 math math: gc_map_comap, map_iInf_comap_of_surjective, comap_inf_map_of_injective, comap_strictMono_of_surjective, FirstOrder.Language.Hom.range_le_iff_comap, map_sup_comap_of_surjective, coe_comap, comap_sup_map_of_injective, comap_surjective_of_injective, comap_id, le_comap_of_map_le, map_comap_le, comap_comap, comap_iSup_map_of_injective, comap_injective_of_surjective, map_iSup_comap_of_surjective, comap_map_eq_of_injective, comap_inf, map_le_iff_le_comap, le_comap_map, comap_iInf, comap_top, map_comap_eq_of_surjective, comap_iInf_map_of_injective, monotone_comap, comap_le_comap_iff_of_surjective, map_comap_map, comap_map_comap, mem_comap, map_inf_comap_of_surjective
copy 📖	CompOp	2 math math: copy_eq, coe_copy
gciMapComap 📖	CompOp	—
gi 📖	CompOp	—
giMapComap 📖	CompOp	—
inclusion 📖	CompOp	18 math math: coe_inclusion, inclusion_self, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, FirstOrder.Language.PartialEquiv.le_iff, FirstOrder.Language.DirectLimit.liftInclusion_of, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, subtype_comp_inclusion, FirstOrder.Language.PartialEquiv.le_def, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, FirstOrder.Language.PartialEquiv.toEquiv_inclusion, FirstOrder.Language.DirectLimit.rangeLiftInclusion
inducedStructure 📖	CompOp	50 math math: FirstOrder.Language.PartialEquiv.toEmbedding_apply, FirstOrder.Language.Embedding.equivRange_toEquiv_apply, FirstOrder.Language.Hom.domRestrict_toFun, subtype_apply, coe_inclusion, inclusion_self, FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure, fg_iff_structure_fg, coe_subtype, cg_iff_structure_cg, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, FirstOrder.Language.PartialEquiv.le_iff, realize_formula_top, FirstOrder.Language.Embedding.subtype_equivRange, FirstOrder.Language.realize_term_substructure, FirstOrder.Language.DirectLimit.liftInclusion_of, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, range_subtype, FirstOrder.Language.Embedding.substructureEquivMap_apply, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, FirstOrder.Language.age.fg_substructure, FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, subtype_injective, subtype_comp_inclusion, FirstOrder.Language.PartialEquiv.le_def, FirstOrder.Language.Hom.subtype_comp_codRestrict, FirstOrder.Language.age.has_representative_as_substructure, coe_topEquiv, FirstOrder.Language.Embedding.comp_codRestrict, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, FirstOrder.Language.PartialEquiv.symm_apply, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, FirstOrder.Language.Embedding.subtype_comp_codRestrict, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, realize_boundedFormula_top, FirstOrder.Language.Embedding.subtype_substructureEquivMap, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, FirstOrder.Language.Embedding.codRestrict_apply, models_of_isUniversal, FirstOrder.Language.Hom.comp_codRestrict, FirstOrder.Language.PartialEquiv.ext_iff, FirstOrder.Language.PartialEquiv.toEquiv_inclusion, FirstOrder.Language.Embedding.domRestrict_apply, FirstOrder.Language.Embedding.equivRange_apply, FirstOrder.Language.DirectLimit.rangeLiftInclusion, FirstOrder.Language.Hom.codRestrict_toFun_coe, FirstOrder.Language.Embedding.codRestrict_apply'
instCompleteLattice 📖	CompOp	31 math math: mem_sSup_of_directedOn, mem_iSup_of_directed, map_sup, map_sup_comap_of_surjective, comap_sup_map_of_injective, small_bot, cg_bot, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, closure_insert, CG.sup, closure_empty, iSup_eq_closure, map_bot, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, closure_iUnion, closure_union, comap_iSup_map_of_injective, FG.sup, map_iSup_comap_of_surjective, elementarySkolem₁Reduct.instSmall, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, instIsEmptySubtypeMemBotOfConstants, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, map_iSup, fg_bot, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, FirstOrder.Language.DirectLimit.range_lift, FirstOrder.Language.DirectLimit.rangeLiftInclusion, FirstOrder.Language.DirectLimit.dom_partialEquivLimit
instInf 📖	CompOp	5 math math: comap_inf_map_of_injective, coe_inf, mem_inf, comap_inf, map_inf_comap_of_surjective
instInfSet 📖	CompOp	7 math math: map_iInf_comap_of_surjective, coe_sInf, comap_iInf, mem_iInf, comap_iInf_map_of_injective, mem_sInf, coe_iInf
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	66 math math: closure_eq_of_isRelational, gc_map_comap, fg_closure_singleton, comap_strictMono_of_surjective, FirstOrder.Language.PartialEquiv.dom_le_dom, FirstOrder.Language.Hom.range_le_iff_comap, small_closure, cg_def, mem_closure, fg_closure, inclusion_self, fg_def, lift_card_closure_le_card_term, FirstOrder.Language.LHom.coe_substructureReduct, mem_closure_iff_exists_term, map_comap_le, skolem₁_reduct_isElementary, FirstOrder.Language.DirectLimit.liftInclusion_of, mem_closed_of_isRelational, fg_iff_exists_fin_generating_family, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, closure_insert, reduct_withConstants, FirstOrder.Language.PartialEquiv.monotone_cod, closure_empty, iSup_eq_closure, monotone_map, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, subset_closure, closure_iUnion, closure_union, FirstOrder.Language.Structure.cg_iff, FirstOrder.Language.PartialEquiv.cod_le_cod, map_le_iff_le_comap, le_comap_map, coe_closure_eq_range_term_realize, closed, FirstOrder.Language.Hom.range_comp_le_range, FirstOrder.Language.PartialEquiv.monotone_dom, FirstOrder.Language.Hom.map_le_range, closure_withConstants_eq, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, map_closure, monotone_comap, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, comap_le_comap_iff_of_surjective, closure_le, mem_closed_iff, Set.Countable.substructure_closure, subset_closure_withConstants, FirstOrder.Language.LHom.mem_substructureReduct, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, cg_iff_empty_or_exists_nat_generating_family, map_le_map_iff_of_injective, FirstOrder.Language.Hom.eqOn_closure, lift_card_closure_le, closure_eq, mem_closure_iff_of_isRelational, closure_mono, FirstOrder.Language.DirectLimit.rangeLiftInclusion, closure_univ, map_strictMono_of_injective, closure_image, cg_closure_singleton, FirstOrder.Language.Structure.fg_iff, cg_closure
instSetLike 📖	CompOp	112 math math: FirstOrder.Language.PartialEquiv.toEmbedding_apply, mem_sSup_of_directedOn, closure_eq_of_isRelational, FirstOrder.Language.IsExtensionPair.cod, mem_iSup_of_directed, FirstOrder.Language.Embedding.equivRange_toEquiv_apply, fg_closure_singleton, ext_iff, small_closure, coe_inf, cg_def, mem_closure, FirstOrder.Language.Hom.domRestrict_toFun, mem_inf, fg_closure, coe_comap, subtype_apply, coe_inclusion, inclusion_self, small_bot, constants_mem, FirstOrder.Language.Hom.mem_range, FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure, FirstOrder.Language.Hom.mem_range_self, fg_iff_structure_fg, coe_subtype, cg_iff_structure_cg, fg_def, coe_sInf, lift_card_closure_le_card_term, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, FirstOrder.Language.LHom.coe_substructureReduct, mem_closure_iff_exists_term, FirstOrder.Language.PartialEquiv.le_iff, realize_formula_top, FirstOrder.Language.Embedding.subtype_equivRange, FirstOrder.Language.realize_term_substructure, coe_top, FirstOrder.Language.DirectLimit.liftInclusion_of, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, range_subtype, FirstOrder.Language.isExtensionPair_iff_cod, FirstOrder.Language.Embedding.substructureEquivMap_apply, mem_closed_of_isRelational, fg_iff_exists_fin_generating_family, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, closure_insert, FirstOrder.Language.age.fg_substructure, closure_empty, FirstOrder.Language.PartialEquiv.toEquiv_inclusion_apply, iSup_eq_closure, FirstOrder.Language.Hom.mem_eqLocus, coe_map, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, subset_closure, closure_iUnion, subtype_injective, closure_union, subtype_comp_inclusion, FirstOrder.Language.Structure.cg_iff, FirstOrder.Language.PartialEquiv.le_def, FG.finite, FirstOrder.Language.age.has_representative_as_substructure, FirstOrder.Language.Hom.range_coe, coe_closure_eq_range_term_realize, closed, coe_topEquiv, coeSort_elementarySkolem₁Reduct, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, mem_carrier, closure_withConstants_eq, FirstOrder.Language.PartialEquiv.symm_apply, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, mem_iInf, map_closure, FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop_apply, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, closure_le, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, mem_closed_iff, instIsEmptySubtypeMemBotOfConstants, Set.Countable.substructure_closure, subset_closure_withConstants, realize_boundedFormula_top, FirstOrder.Language.LHom.mem_substructureReduct, FirstOrder.Language.Embedding.subtype_substructureEquivMap, mem_sInf, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, cg_iff_empty_or_exists_nat_generating_family, coe_iInf, cg_iff_countable, FirstOrder.Language.Hom.eqOn_closure, models_of_isUniversal, mem_map, mem_comap, mem_top, FirstOrder.Language.PartialEquiv.ext_iff, FirstOrder.Language.PartialEquiv.toEquiv_inclusion, FirstOrder.Language.Embedding.domRestrict_apply, lift_card_closure_le, closure_eq, FirstOrder.Language.Embedding.equivRange_apply, mem_closure_iff_of_isRelational, closure_mono, FirstOrder.Language.DirectLimit.rangeLiftInclusion, closure_univ, closure_image, apply_coe_mem_map, fg_iff_finite, cg_closure_singleton, FirstOrder.Language.Structure.fg_iff, cg_closure
instTop 📖	CompOp	19 math math: FirstOrder.Language.Structure.fg_def, FirstOrder.Language.Hom.range_le_iff_comap, realize_formula_top, coe_top, FirstOrder.Language.Hom.range_eq_map, FirstOrder.Language.Structure.cg_def, FirstOrder.Language.Hom.range_id, FirstOrder.Language.Structure.cg_iff, FirstOrder.Language.Equiv.toHom_range, coe_topEquiv, comap_top, FirstOrder.Language.Hom.range_eq_top, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, realize_boundedFormula_top, FirstOrder.Language.Structure.CG.out, FirstOrder.Language.Structure.FG.out, mem_top, closure_univ, FirstOrder.Language.Structure.fg_iff
map 📖	CompOp	41 math math: gc_map_comap, map_iInf_comap_of_surjective, comap_inf_map_of_injective, map_sup, map_map, map_sup_comap_of_surjective, comap_sup_map_of_injective, CG.map, map_comap_le, FirstOrder.Language.Hom.range_eq_map, FirstOrder.Language.Embedding.substructureEquivMap_apply, FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma, map_bot, coe_map, monotone_map, map_injective_of_injective, comap_iSup_map_of_injective, map_iSup_comap_of_surjective, comap_map_eq_of_injective, map_le_iff_le_comap, le_comap_map, map_id, map_le_of_le_comap, FirstOrder.Language.Hom.map_le_range, map_comap_eq_of_surjective, comap_iInf_map_of_injective, map_closure, map_comap_map, FirstOrder.Language.Hom.range_comp, FirstOrder.Language.Embedding.subtype_substructureEquivMap, comap_map_comap, map_iSup, map_le_map_iff_of_injective, FG.map, map_surjective_of_surjective, mem_map_of_mem, mem_map, map_inf_comap_of_surjective, map_strictMono_of_injective, closure_image, apply_coe_mem_map
subtype 📖	CompOp	13 math math: subtype_apply, coe_subtype, FirstOrder.Language.Embedding.subtype_equivRange, FirstOrder.Language.DirectLimit.liftInclusion_of, FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion, range_subtype, subtype_injective, subtype_comp_inclusion, FirstOrder.Language.PartialEquiv.le_def, FirstOrder.Language.Hom.subtype_comp_codRestrict, FirstOrder.Language.Embedding.subtype_comp_codRestrict, FirstOrder.Language.Embedding.subtype_substructureEquivMap, FirstOrder.Language.PartialEquiv.ext_iff
topEquiv 📖	CompOp	1 math math: coe_topEquiv
withConstants 📖	CompOp	4 math math: reduct_withConstants, coe_withConstants, mem_withConstants, closure_withConstants_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_coe_mem_map 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike map DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	mem_map_of_mem Subtype.prop
closed 📖	mathematical	—	LowerAdjoint.closed Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure	—	LowerAdjoint.eq_of_le Set.Subset.rfl mem_closure
closure_empty 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot GaloisInsertion.gc
closure_eq 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure	—	GaloisInsertion.l_u_eq
closure_eq_of_isRelational 📖	mathematical	FirstOrder.Language.IsRelational	SetLike.coe FirstOrder.Language.Substructure instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder closure	—	LowerAdjoint.closure_eq_self_of_mem_closed mem_closed_of_isRelational
closure_eq_of_le 📖	—	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure instSetLike Preorder.toLE PartialOrder.toPreorder instPartialOrder LowerAdjoint.toFun OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra closure	—	—	LowerAdjoint.eq_of_le
closure_iUnion 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_iSup GaloisInsertion.gc
closure_image 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.image DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike map	—	map_closure
closure_induction 📖	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure FirstOrder.Language.ClosedUnder setOf	—	—	closure_le
closure_induction' 📖	—	subset_closure FirstOrder.Language.ClosedUnder setOf FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure	—	—	subset_closure closure_induction
closure_insert 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.instInsert SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set.instSingletonSet	—	closure_union
closure_le 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder LowerAdjoint.toFun Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.coe instSetLike closure Set.instHasSubset	—	LowerAdjoint.closure_le_closed_iff_le closed
closure_mono 📖	mathematical	Set Set.instHasSubset	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder LowerAdjoint.toFun OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.coe instSetLike closure	—	LowerAdjoint.monotone
closure_union 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.instUnion SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_sup GaloisInsertion.gc
closure_univ 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.univ Top.top instTop	—	closure_eq coe_top
closure_withConstants_eq 📖	mathematical	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure FirstOrder.Language.withConstants Set.Elem FirstOrder.Language.withConstantsStructure FirstOrder.Language.paramsStructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure withConstants Set.instUnion HasSubset.Subset.trans Set.instHasSubset Set.instIsTransSubset Set.subset_union_left subset_closure	—	closure_eq_of_le HasSubset.Subset.trans Set.instIsTransSubset Set.subset_union_left subset_closure Set.subset_union_right FirstOrder.Language.withConstants_expansion OrderEmbedding.le_iff_le reduct_withConstants subset_closure_withConstants
coe_closure_eq_range_term_realize 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder closure Set.range FirstOrder.Language.Term Set.instMembership FirstOrder.Language.Term.realize	—	SetLike.ext'_iff closure_eq_of_le le_sInf FirstOrder.Language.Term.realize_mem
coe_comap 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike comap Set.preimage DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	—
coe_copy 📖	mathematical	SetLike.coe FirstOrder.Language.Substructure instSetLike	copy	—	—
coe_iInf 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike iInf instInfSet Set.iInter	—	Set.biInter_range
coe_inclusion 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe FirstOrder.Language.Embedding SetLike.instMembership instSetLike inducedStructure FirstOrder.Language.Embedding.funLike inclusion Set.inclusion SetLike.coe	—	—
coe_inf 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike instInf Set Set.instInter	—	—
coe_map 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike map Set.image DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	—
coe_sInf 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	—
coe_subtype 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership instSetLike inducedStructure FirstOrder.Language.Embedding.funLike subtype	—	—
coe_top 📖	mathematical	—	SetLike.coe FirstOrder.Language.Substructure instSetLike Top.top instTop Set.univ	—	—
coe_topEquiv 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Equiv FirstOrder.Language.Substructure SetLike.instMembership instSetLike Top.top instTop inducedStructure EquivLike.toFunLike FirstOrder.Language.Equiv.instEquivLike topEquiv	—	—
coe_withConstants 📖	mathematical	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure instSetLike	FirstOrder.Language.withConstants Set.Elem FirstOrder.Language.withConstantsStructure FirstOrder.Language.paramsStructure withConstants	—	—
comap_comap 📖	mathematical	—	comap FirstOrder.Language.Hom.comp	—	—
comap_iInf 📖	mathematical	—	comap iInf FirstOrder.Language.Substructure instInfSet	—	GaloisConnection.u_iInf gc_map_comap
comap_iInf_map_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	comap iInf FirstOrder.Language.Substructure instInfSet map	—	GaloisCoinsertion.u_iInf_l
comap_iSup_map_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	comap iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice map	—	GaloisCoinsertion.u_iSup_l
comap_id 📖	mathematical	—	comap FirstOrder.Language.Hom.id	—	ext
comap_inf 📖	mathematical	—	comap FirstOrder.Language.Substructure instInf	—	GaloisConnection.u_inf gc_map_comap
comap_inf_map_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	comap FirstOrder.Language.Substructure instInf map	—	GaloisCoinsertion.u_inf_l
comap_injective_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure comap	—	GaloisInsertion.u_injective
comap_le_comap_iff_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder comap	—	GaloisInsertion.u_le_u_iff
comap_map_comap 📖	mathematical	—	comap map	—	GaloisConnection.u_l_u_eq_u gc_map_comap
comap_map_eq_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	comap map	—	GaloisCoinsertion.u_l_eq
comap_strictMono_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	StrictMono FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder comap	—	GaloisInsertion.strictMono_u
comap_sup_map_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	comap FirstOrder.Language.Substructure SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice map	—	GaloisCoinsertion.u_sup_l
comap_surjective_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure comap	—	GaloisCoinsertion.u_surjective
comap_top 📖	mathematical	—	comap Top.top FirstOrder.Language.Substructure instTop	—	GaloisConnection.u_top gc_map_comap
constants_mem 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike FirstOrder.Language.constantMap	—	mem_carrier fun_mem Fin.isEmpty'
copy_eq 📖	mathematical	SetLike.coe FirstOrder.Language.Substructure instSetLike	copy	—	SetLike.coe_injective
dense_induction 📖	—	LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Top.top instTop FirstOrder.Language.ClosedUnder setOf	—	—	closure_induction
ext 📖	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike	—	ext
fun_mem 📖	mathematical	—	FirstOrder.Language.ClosedUnder carrier	—	—
gc_map_comap 📖	mathematical	—	GaloisConnection FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder map comap	—	map_le_iff_le_comap
iSup_eq_closure 📖	mathematical	—	iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.iUnion	—	closure_iUnion closure_eq
inclusion_self 📖	mathematical	—	inclusion le_refl FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder FirstOrder.Language.Embedding.refl SetLike.instMembership instSetLike inducedStructure	—	le_refl
instIsEmptySubtypeMemBotOfConstants 📖	mathematical	—	IsEmpty FirstOrder.Language.Substructure SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	isEmpty_subtype mem_closed_iff closure_empty SetLike.mem_coe Set.notMem_empty
le_comap_map 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder comap map	—	GaloisConnection.le_u_l gc_map_comap
le_comap_of_map_le 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder map	comap	—	GaloisConnection.le_u gc_map_comap
lift_card_closure_le 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0 Cardinal.instAdd Set.Elem FirstOrder.Language.Functions	—	Cardinal.lift_umax LE.le.trans lift_card_closure_le_card_term FirstOrder.Language.Term.card_le Cardinal.mk_sum le_refl
lift_card_closure_le_card_term 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure FirstOrder.Language.Term Set.Elem	—	SetLike.coe_sort_coe coe_closure_eq_range_term_realize Cardinal.lift_id' Cardinal.mk_range_le_lift
map_bot 📖	mathematical	—	map Bot.bot FirstOrder.Language.Substructure OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	GaloisConnection.l_bot gc_map_comap
map_closure 📖	mathematical	—	map LowerAdjoint.toFun Set FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure Set.image DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	closure_eq_of_le Set.image_mono subset_closure map_le_iff_le_comap closure_le
map_comap_eq_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	map comap	—	GaloisInsertion.l_u_eq
map_comap_le 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	GaloisConnection.l_u_le gc_map_comap
map_comap_map 📖	mathematical	—	map comap	—	GaloisConnection.l_u_l_eq_l gc_map_comap
map_iInf_comap_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	map iInf FirstOrder.Language.Substructure instInfSet comap	—	GaloisInsertion.l_iInf_u
map_iSup 📖	mathematical	—	map iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_iSup gc_map_comap
map_iSup_comap_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	map iSup FirstOrder.Language.Substructure ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice comap	—	GaloisInsertion.l_iSup_u
map_id 📖	mathematical	—	map FirstOrder.Language.Hom.id	—	SetLike.coe_injective Set.image_id
map_inf_comap_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	map FirstOrder.Language.Substructure instInf comap	—	GaloisInsertion.l_inf_u
map_injective_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure map	—	GaloisCoinsertion.l_injective
map_le_iff_le_comap 📖	mathematical	—	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	Set.image_subset_iff
map_le_map_iff_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder map	—	GaloisCoinsertion.l_le_l_iff
map_le_of_le_comap 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder comap	map	—	GaloisConnection.l_le gc_map_comap
map_map 📖	mathematical	—	map FirstOrder.Language.Hom.comp	—	SetLike.coe_injective Set.image_image
map_strictMono_of_injective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	StrictMono FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder map	—	GaloisCoinsertion.strictMono_l
map_sup 📖	mathematical	—	map FirstOrder.Language.Substructure SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	GaloisConnection.l_sup gc_map_comap
map_sup_comap_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	map FirstOrder.Language.Substructure SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice comap	—	GaloisInsertion.l_sup_u
map_surjective_of_surjective 📖	mathematical	DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	FirstOrder.Language.Substructure map	—	GaloisInsertion.l_surjective
mem_carrier 📖	mathematical	—	Set Set.instMembership carrier FirstOrder.Language.Substructure SetLike.instMembership instSetLike	—	—
mem_closed_iff 📖	mathematical	—	Set Set.instMembership LowerAdjoint.closed FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure FirstOrder.Language.ClosedUnder	—	fun_mem closure_eq_of_le refl Set.instReflSubset subset_closure
mem_closed_of_isRelational 📖	mathematical	FirstOrder.Language.IsRelational	Set Set.instMembership LowerAdjoint.closed FirstOrder.Language.Substructure PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe instSetLike closure	—	mem_closed_iff
mem_closure 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure	—	mem_sInf
mem_closure_iff_exists_term 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure FirstOrder.Language.Term.realize Set.instMembership	—	SetLike.mem_coe coe_closure_eq_range_term_realize Set.mem_range
mem_closure_iff_of_isRelational 📖	mathematical	FirstOrder.Language.IsRelational	FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure Set.instMembership	—	SetLike.mem_coe closure_eq_of_isRelational
mem_comap 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike comap DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	—
mem_iInf 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike iInf instInfSet	—	—
mem_iSup_of_directed 📖	mathematical	Directed FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	closure_induction Set.mem_iUnion Directed.finite_le instIsTransLe Finite.of_fintype fun_mem closure_iUnion closure_eq le_iSup
mem_inf 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike instInf	—	—
mem_map 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike map DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	—
mem_map_of_mem 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership instSetLike	map DFunLike.coe FirstOrder.Language.Hom FirstOrder.Language.Hom.instFunLike	—	Set.mem_image_of_mem
mem_sInf 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike InfSet.sInf instInfSet	—	Set.mem_iInter₂
mem_sSup_of_directedOn 📖	mathematical	Set.Nonempty FirstOrder.Language.Substructure DirectedOn Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instMembership	—	sSup_eq_iSup' mem_iSup_of_directed Set.Nonempty.to_subtype DirectedOn.directed_val
mem_top 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike Top.top instTop	—	Set.mem_univ
mem_withConstants 📖	mathematical	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure instSetLike	FirstOrder.Language.withConstants Set.Elem FirstOrder.Language.withConstantsStructure FirstOrder.Language.paramsStructure SetLike.instMembership withConstants	—	—
monotone_comap 📖	mathematical	—	Monotone FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder comap	—	GaloisConnection.monotone_u gc_map_comap
monotone_map 📖	mathematical	—	Monotone FirstOrder.Language.Substructure PartialOrder.toPreorder instPartialOrder map	—	GaloisConnection.monotone_l gc_map_comap
notMem_of_notMem_closure 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure	Set.instMembership	—	subset_closure
range_subtype 📖	mathematical	—	FirstOrder.Language.Hom.range FirstOrder.Language.Substructure SetLike.instMembership instSetLike inducedStructure FirstOrder.Language.Embedding.toHom subtype	—	ext
realize_boundedFormula_top 📖	mathematical	—	FirstOrder.Language.BoundedFormula.Realize FirstOrder.Language.Substructure SetLike.instMembership instSetLike Top.top instTop inducedStructure	—	FirstOrder.Language.StrongHomClass.realize_boundedFormula FirstOrder.Language.Equiv.instStrongHomClass
realize_formula_top 📖	mathematical	—	FirstOrder.Language.Formula.Realize FirstOrder.Language.Substructure SetLike.instMembership instSetLike Top.top instTop inducedStructure	—	FirstOrder.Language.StrongHomClass.realize_formula FirstOrder.Language.Equiv.instStrongHomClass
reduct_withConstants 📖	mathematical	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure instSetLike	DFunLike.coe OrderEmbedding FirstOrder.Language.withConstants Set.Elem FirstOrder.Language.withConstantsStructure FirstOrder.Language.paramsStructure Preorder.toLE PartialOrder.toPreorder instPartialOrder instFunLikeOrderEmbedding FirstOrder.Language.LHom.substructureReduct FirstOrder.Language.lhomWithConstants FirstOrder.Language.withConstants_expansion withConstants	—	ext FirstOrder.Language.withConstants_expansion
small_bot 📖	mathematical	—	Small FirstOrder.Language.Substructure SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	closure_empty small_closure small_subsingleton IsEmpty.instSubsingleton Set.instIsEmptyElemEmptyCollection
small_closure 📖	mathematical	—	Small FirstOrder.Language.Substructure SetLike.instMembership instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder SetLike.coe closure	—	SetLike.coe_sort_coe coe_closure_eq_range_term_realize small_range FirstOrder.Language.Term.small
subset_closure 📖	mathematical	—	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure instSetLike LowerAdjoint.toFun PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder closure	—	LowerAdjoint.le_closure
subset_closure_withConstants 📖	mathematical	—	Set Set.instHasSubset SetLike.coe FirstOrder.Language.Substructure FirstOrder.Language.withConstants Set.Elem FirstOrder.Language.withConstantsStructure FirstOrder.Language.paramsStructure instSetLike LowerAdjoint.toFun PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder closure	—	constants_mem
subtype_apply 📖	mathematical	—	DFunLike.coe FirstOrder.Language.Embedding FirstOrder.Language.Substructure SetLike.instMembership instSetLike inducedStructure FirstOrder.Language.Embedding.funLike subtype	—	—
subtype_comp_inclusion 📖	mathematical	FirstOrder.Language.Substructure Preorder.toLE PartialOrder.toPreorder instPartialOrder	FirstOrder.Language.Embedding.comp SetLike.instMembership instSetLike inducedStructure subtype inclusion	—	—
subtype_injective 📖	mathematical	—	FirstOrder.Language.Substructure SetLike.instMembership instSetLike DFunLike.coe FirstOrder.Language.Embedding inducedStructure FirstOrder.Language.Embedding.funLike subtype	—	Subtype.coe_injective

FirstOrder.Language.Term

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_mem 📖	mathematical	FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike	realize	—	FirstOrder.Language.Substructure.fun_mem

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
substructure_closure 📖	mathematical	—	Countable FirstOrder.Language.Substructure SetLike.instMembership FirstOrder.Language.Substructure.instSetLike LowerAdjoint.toFun Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra FirstOrder.Language.Substructure.instPartialOrder SetLike.coe FirstOrder.Language.Substructure.closure	—	Cardinal.mk_le_aleph0_iff Cardinal.lift_le_aleph0 LE.le.trans FirstOrder.Language.Substructure.lift_card_closure_le_card_term Cardinal.mk_le_aleph0 FirstOrder.Language.Term.instCountableOfSigmaNatFunctions to_subtype

---

← Back to Index