CompleteLattice

📁 Source: Mathlib/Order/Hom/CompleteLattice.lean

Statistics

Metric	Count
Definitions CompleteLatticeHom, comp, copy, dual, id, instFunLike, instInhabited, setPreimage, toBoundedLatticeHom, tosInfHom, tosSupHom, CompleteLatticeHomClass, toOrderIsoSet, FrameHom, comp, copy, id, instFunLike, instInhabited, instPartialOrder, toInfTopHom, toLatticeHom, FrameHomClass, toCompleteLatticeHom, infsInfHom, instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass, instCoeTCFrameHomOfFrameHomClass, instCoeTCSInfHomOfSInfHomClass, instCoeTCSSupHomOfSSupHomClass, sInfHom, comp, copy, dual, id, instFunLike, instInhabited, instOrderTop, instPartialOrder, instTop, toFun, sInfHomClass, sSupHom, comp, copy, dual, id, instBot, instFunLike, instInhabited, instOrderBot, instPartialOrder, setImage, toFun, sSupHomClass, supsSupHom	55
Theorems cancel_left, cancel_right, coe_comp, coe_copy, coe_id, coe_mk, coe_setPreimage, coe_toBoundedLatticeHom, coe_tosInfHom, coe_tosSupHom, comp_apply, comp_assoc, comp_id, copy_eq, dual_apply_toFun, dual_comp, dual_id, dual_symm_apply_toFun, ext, ext_iff, id_apply, id_comp, instCompleteLatticeHomClass, map_sSup', setPreimage_apply, setPreimage_comp, setPreimage_id, symm_dual_comp, symm_dual_id, toFun_eq_coe, toBoundedLatticeHomClass, toFrameHomClass, tosInfHomClass, tosSupHomClass, toOrderIsoSet_apply, toOrderIsoSet_symm_apply, cancel_left, cancel_right, coe_comp, coe_copy, coe_id, coe_mk, coe_toInfTopHom, coe_toLatticeHom, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instFrameHomClass, map_sSup', toFun_eq_coe, map_sSup, toBoundedLatticeHomClass, toInfTopHomClass, tosSupHomClass, toCompleteLatticeHom_toFun, toCompleteLatticeHomClass, tosInfHomClass, tosSupHomClass, image_sSup, infsInfHom_apply, map_iInf, map_iInf₂, map_iSup, map_iSup₂, cancel_left, cancel_right, coe_comp, coe_copy, coe_id, coe_mk, coe_top, comp_apply, comp_assoc, comp_id, copy_eq, dual_apply_toFun, dual_comp, dual_id, dual_symm_apply_toFun, ext, ext_iff, id_apply, id_comp, instSInfHomClass, map_sInf', symm_dual_comp, symm_dual_id, toFun_eq_coe, top_apply, map_sInf, toInfTopHomClass, bot_apply, cancel_left, cancel_right, coe_bot, coe_comp, coe_copy, coe_id, coe_mk, comp_apply, comp_assoc, comp_id, copy_eq, dual_apply_toFun, dual_comp, dual_id, dual_symm_apply_toFun, ext, ext_iff, id_apply, id_comp, instSSupHomClass, map_sSup', setImage_toFun, symm_dual_comp, symm_dual_id, toFun_eq_coe, map_sSup, toSupBotHomClass, supsSupHom_apply	125
Total	180

CompleteLatticeHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	10 math math: cancel_right, coe_comp, comp_id, comp_apply, comp_assoc, id_comp, cancel_left, dual_comp, setPreimage_comp, symm_dual_comp
copy 📖	CompOp	2 math math: copy_eq, coe_copy
dual 📖	CompOp	7 math math: dual_symm_apply_toFun, dual_id, symm_dual_id, CompleteLat.dual_map, dual_apply_toFun, dual_comp, symm_dual_comp
id 📖	CompOp	7 math math: coe_id, dual_id, comp_id, id_comp, symm_dual_id, setPreimage_id, id_apply
instFunLike 📖	CompOp	30 math math: range_coe, coe_toBoundedLatticeHom, coe_tosSupHom, dual_symm_apply_toFun, coe_comp, apply_limsup_iterate, coe_id, toFun_eq_coe, setPreimage_apply, CompleteSublattice.mem_subtype, ext_iff, comp_apply, apply_liminf_iterate, CompleteSublattice.mem_map, coe_mk, CompleteSublattice.subtype_injective, CompleteLat.Iso.mk_hom, coe_tosInfHom, completeLat_dual_comp_forget_to_bddLat, instCompleteLatticeHomClass, CompleteSublattice.coe_subtype, CompleteSublattice.comap_carrier, CompleteSublattice.mem_comap, dual_apply_toFun, toOrderIsoRangeOfInjective_apply, coe_setPreimage, coe_copy, CompleteSublattice.map_carrier, CompleteLat.Iso.mk_inv, id_apply
instInhabited 📖	CompOp	—
setPreimage 📖	CompOp	4 math math: setPreimage_apply, coe_setPreimage, setPreimage_id, setPreimage_comp
toBoundedLatticeHom 📖	CompOp	1 math math: coe_toBoundedLatticeHom
tosInfHom 📖	CompOp	6 math math: dual_symm_apply_toFun, toFun_eq_coe, map_sSup', coe_tosInfHom, dual_apply_toFun, OrderIso.toCompleteLatticeHom_toFun
tosSupHom 📖	CompOp	1 math math: coe_tosSupHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe CompleteLatticeHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe CompleteLatticeHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe CompleteLatticeHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe CompleteLatticeHom instFunLike	DFunLike.coe CompleteLatticeHom instFunLike copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe CompleteLatticeHom instFunLike id	—	—
coe_mk 📖	mathematical	sInfHom.toFun CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Set.image	DFunLike.coe CompleteLatticeHom instFunLike sInfHom CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf sInfHom.instFunLike	—	—
coe_setPreimage 📖	mathematical	—	DFunLike.coe CompleteLatticeHom Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instFunLike setPreimage Set.preimage	—	—
coe_toBoundedLatticeHom 📖	mathematical	—	DFunLike.coe BoundedLatticeHom CompleteLattice.toLattice CompleteLattice.toBoundedOrder BoundedLatticeHom.instFunLike toBoundedLatticeHom CompleteLatticeHom instFunLike	—	—
coe_tosInfHom 📖	mathematical	—	DFunLike.coe sInfHom CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf sInfHom.instFunLike tosInfHom CompleteLatticeHom instFunLike	—	—
coe_tosSupHom 📖	mathematical	—	DFunLike.coe sSupHom CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup sSupHom.instFunLike tosSupHom CompleteLatticeHom instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe CompleteLatticeHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe CompleteLatticeHom instFunLike	copy	—	DFunLike.ext'
dual_apply_toFun 📖	mathematical	—	sInfHom.toFun OrderDual CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf OrderDual.instCompleteLattice tosInfHom DFunLike.coe Equiv CompleteLatticeHom EquivLike.toFunLike Equiv.instEquivLike dual OrderDual.toDual instFunLike OrderDual.ofDual	—	—
dual_comp 📖	mathematical	—	DFunLike.coe Equiv CompleteLatticeHom OrderDual OrderDual.instCompleteLattice EquivLike.toFunLike Equiv.instEquivLike dual comp	—	—
dual_id 📖	mathematical	—	DFunLike.coe Equiv CompleteLatticeHom OrderDual OrderDual.instCompleteLattice EquivLike.toFunLike Equiv.instEquivLike dual id	—	—
dual_symm_apply_toFun 📖	mathematical	—	sInfHom.toFun CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf tosInfHom DFunLike.coe Equiv CompleteLatticeHom OrderDual OrderDual.instCompleteLattice EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual OrderDual.toDual instFunLike OrderDual.ofDual	—	—
ext 📖	—	DFunLike.coe CompleteLatticeHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CompleteLatticeHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe CompleteLatticeHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instCompleteLatticeHomClass 📖	mathematical	—	CompleteLatticeHomClass CompleteLatticeHom instFunLike	—	sInfHom.map_sInf' map_sSup'
map_sSup' 📖	mathematical	—	sInfHom.toFun CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf tosInfHom SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Set.image	—	—
setPreimage_apply 📖	mathematical	—	DFunLike.coe CompleteLatticeHom Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instFunLike setPreimage Set.preimage	—	—
setPreimage_comp 📖	mathematical	—	setPreimage comp Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	—
setPreimage_id 📖	mathematical	—	setPreimage id Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	—	—
symm_dual_comp 📖	mathematical	—	DFunLike.coe Equiv CompleteLatticeHom OrderDual OrderDual.instCompleteLattice EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual comp	—	—
symm_dual_id 📖	mathematical	—	DFunLike.coe Equiv CompleteLatticeHom OrderDual OrderDual.instCompleteLattice EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual id	—	—
toFun_eq_coe 📖	mathematical	—	sInfHom.toFun CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf tosInfHom DFunLike.coe CompleteLatticeHom instFunLike	—	—

CompleteLatticeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBoundedLatticeHomClass 📖	mathematical	—	BoundedLatticeHomClass CompleteLattice.toLattice CompleteLattice.toBoundedOrder	—	sSupHomClass.toSupBotHomClass tosSupHomClass sInfHomClass.toInfTopHomClass tosInfHomClass SupBotHomClass.toSupHomClass InfTopHomClass.toInfHomClass InfTopHomClass.map_top SupBotHomClass.map_bot
toFrameHomClass 📖	mathematical	—	FrameHomClass	—	sInfHomClass.toInfTopHomClass tosInfHomClass sSupHomClass.map_sSup tosSupHomClass
tosInfHomClass 📖	mathematical	—	sInfHomClass CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf	—	—
tosSupHomClass 📖	mathematical	—	sSupHomClass CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	—

Equiv

Definitions

Name	Category	Theorems
toOrderIsoSet 📖	CompOp	2 math math: toOrderIsoSet_symm_apply, toOrderIsoSet_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toOrderIsoSet_apply 📖	mathematical	—	DFunLike.coe RelIso Set Set.instLE RelIso.instFunLike toOrderIsoSet Set.image Equiv EquivLike.toFunLike instEquivLike	—	—
toOrderIsoSet_symm_apply 📖	mathematical	—	DFunLike.coe RelIso Set Set.instLE RelIso.instFunLike RelIso.symm toOrderIsoSet Set.image Equiv EquivLike.toFunLike instEquivLike symm	—	—

FrameHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	10 math math: comp_id, id_comp, cancel_left, coe_comp, Frm.hom_comp, TopologicalSpace.Opens.comap_comp, Frm.ofHom_comp, cancel_right, comp_assoc, comp_apply
copy 📖	CompOp	2 math math: copy_eq, coe_copy
id 📖	CompOp	7 math math: comp_id, id_comp, coe_id, Frm.ofHom_id, Frm.hom_id, TopologicalSpace.Opens.comap_id, id_apply
instFunLike 📖	CompOp	46 math math: Frm.coe_comp, TopologicalSpace.Opens.comap_mono, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, Locale.localePointOfSpacePoint_toFun, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, Homeomorph.opensCongr_apply, Nucleus.restrict_toFun, TopologicalSpace.Opens.comap_comap, TopologicalSpace.IsOpenCover.comap, TopologicalSpace.Opens.mem_comap, TopologicalSpace.Opens.frameHom_toFun, IsLocalization.mapFrameHom_apply, Frm.ext_iff, MeasureTheory.Content.is_mul_left_invariant_innerContent, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, coe_toLatticeHom, coe_comp, Submodule.IsLocalizedModule.localized₀FrameHom_apply, coe_id, Frm.id_apply, Frm.coe_id, coe_toInfTopHom, Frm.inv_hom_apply, Locale.PT.isOpen_iff, Frm.hom_inv_apply, Locale.openOfElementHom_toFun, Submodule.IsLocalizedModule.localized'FrameHom_apply, PrimeSpectrum.comap_basicOpen, coe_mk, MeasureTheory.Content.is_add_left_invariant_innerContent, TopologicalSpace.Opens.coe_comap, Frm.ofHom_apply, ext_iff, Nucleus.restrict_toSublocale, Frm.comp_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, toFun_eq_coe, Frm.forget_map, MeasureTheory.Content.innerContent_comap, Sublocale.restrict_of_mem, id_apply, Sublocale.toNucleus_apply, comp_apply, coe_copy, instFrameHomClass
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	—
toInfTopHom 📖	CompOp	3 math math: coe_toInfTopHom, map_sSup', toFun_eq_coe
toLatticeHom 📖	CompOp	1 math math: coe_toLatticeHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe FrameHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe FrameHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe FrameHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe FrameHom instFunLike	DFunLike.coe FrameHom instFunLike copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe FrameHom instFunLike id	—	—
coe_mk 📖	mathematical	InfHom.toFun SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice InfTopHom.toInfHom OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Set.image	DFunLike.coe FrameHom instFunLike InfTopHom SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder InfTopHom.instFunLike	—	—
coe_toInfTopHom 📖	mathematical	—	DFunLike.coe InfTopHom SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder InfTopHom.instFunLike toInfTopHom FrameHom instFunLike	—	—
coe_toLatticeHom 📖	mathematical	—	DFunLike.coe LatticeHom CompleteLattice.toLattice LatticeHom.instFunLike toLatticeHom FrameHom instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe FrameHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe FrameHom instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe FrameHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe FrameHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe FrameHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instFrameHomClass 📖	mathematical	—	FrameHomClass FrameHom instFunLike	—	InfHom.map_inf' InfTopHom.map_top' map_sSup'
map_sSup' 📖	mathematical	—	InfHom.toFun SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice InfTopHom.toInfHom OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toInfTopHom SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Set.image	—	—
toFun_eq_coe 📖	mathematical	—	InfHom.toFun SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice InfTopHom.toInfHom OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder toInfTopHom DFunLike.coe FrameHom instFunLike	—	—

FrameHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_sSup 📖	mathematical	—	DFunLike.coe SupSet.sSup CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Set.image	—	—
toBoundedLatticeHomClass 📖	mathematical	—	BoundedLatticeHomClass CompleteLattice.toLattice CompleteLattice.toBoundedOrder	—	sSupHomClass.toSupBotHomClass tosSupHomClass SupBotHomClass.toSupHomClass InfTopHomClass.toInfHomClass toInfTopHomClass InfTopHomClass.map_top SupBotHomClass.map_bot
toInfTopHomClass 📖	mathematical	—	InfTopHomClass SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
tosSupHomClass 📖	mathematical	—	sSupHomClass CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup	—	map_sSup

OrderIso

Definitions

Name	Category	Theorems
toCompleteLatticeHom 📖	CompOp	1 math math: toCompleteLatticeHom_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompleteLatticeHom_toFun 📖	mathematical	—	sInfHom.toFun CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf CompleteLatticeHom.tosInfHom toCompleteLatticeHom DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder instFunLikeOrderIso	—	—

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toCompleteLatticeHomClass 📖	mathematical	—	CompleteLatticeHomClass EquivLike.toFunLike	—	tosSupHomClass tosInfHomClass
tosInfHomClass 📖	mathematical	—	sInfHomClass CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf EquivLike.toFunLike	—	eq_of_forall_le_iff map_inv_le_iff le_sInf_iff Set.forall_mem_image
tosSupHomClass 📖	mathematical	—	sSupHomClass CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup EquivLike.toFunLike	—	eq_of_forall_ge_iff

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_sSup 📖	mathematical	—	image SupSet.sSup Set instSupSet	—	image_sUnion

(root)

Definitions

Name	Category	Theorems
CompleteLatticeHom 📖	CompData	35 math math: CompleteLatticeHom.range_coe, CompleteLatticeHom.coe_toBoundedLatticeHom, CompleteLatticeHom.coe_tosSupHom, CompleteLatticeHom.dual_symm_apply_toFun, CompleteLatticeHom.coe_comp, CompleteLatticeHom.apply_limsup_iterate, CompleteLatticeHom.coe_id, CompleteLatticeHom.dual_id, CompleteLatticeHom.toFun_eq_coe, CompleteLatticeHom.setPreimage_apply, CompleteSublattice.mem_subtype, CompleteLatticeHom.ext_iff, CompleteLatticeHom.comp_apply, CompleteLatticeHom.apply_liminf_iterate, CompleteSublattice.mem_map, CompleteLatticeHom.coe_mk, CompleteLatticeHom.symm_dual_id, CompleteLat.dual_map, CompleteSublattice.subtype_injective, CompleteLat.Iso.mk_hom, CompleteLatticeHom.coe_tosInfHom, completeLat_dual_comp_forget_to_bddLat, CompleteLatticeHom.instCompleteLatticeHomClass, CompleteSublattice.coe_subtype, CompleteSublattice.comap_carrier, CompleteSublattice.mem_comap, CompleteLatticeHom.dual_apply_toFun, CompleteLatticeHom.toOrderIsoRangeOfInjective_apply, CompleteLatticeHom.coe_setPreimage, CompleteLatticeHom.dual_comp, CompleteLatticeHom.coe_copy, CompleteSublattice.map_carrier, CompleteLatticeHom.symm_dual_comp, CompleteLat.Iso.mk_inv, CompleteLatticeHom.id_apply
CompleteLatticeHomClass 📖	CompData	2 math math: CompleteLatticeHom.instCompleteLatticeHomClass, OrderIsoClass.toCompleteLatticeHomClass
FrameHom 📖	CompData	46 math math: Frm.coe_comp, TopologicalSpace.Opens.comap_mono, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, Locale.localePointOfSpacePoint_toFun, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, Homeomorph.opensCongr_apply, Nucleus.restrict_toFun, TopologicalSpace.Opens.comap_comap, TopologicalSpace.IsOpenCover.comap, TopologicalSpace.Opens.mem_comap, TopologicalSpace.Opens.frameHom_toFun, IsLocalization.mapFrameHom_apply, Frm.ext_iff, MeasureTheory.Content.is_mul_left_invariant_innerContent, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, FrameHom.coe_toLatticeHom, FrameHom.coe_comp, Submodule.IsLocalizedModule.localized₀FrameHom_apply, FrameHom.coe_id, Frm.id_apply, Frm.coe_id, FrameHom.coe_toInfTopHom, Frm.inv_hom_apply, Frm.hom_inv_apply, Locale.openOfElementHom_toFun, Submodule.IsLocalizedModule.localized'FrameHom_apply, PrimeSpectrum.comap_basicOpen, FrameHom.coe_mk, TopologicalSpace.Opens.comap_injective, MeasureTheory.Content.is_add_left_invariant_innerContent, TopologicalSpace.Opens.coe_comap, Frm.ofHom_apply, FrameHom.ext_iff, Nucleus.restrict_toSublocale, Frm.comp_apply, AlgebraicGeometry.StructureSheaf.comap_basicOpen, FrameHom.toFun_eq_coe, Frm.forget_map, MeasureTheory.Content.innerContent_comap, Sublocale.restrict_of_mem, FrameHom.id_apply, Sublocale.toNucleus_apply, FrameHom.comp_apply, FrameHom.coe_copy, FrameHom.instFrameHomClass
FrameHomClass 📖	CompData	2 math math: CompleteLatticeHomClass.toFrameHomClass, FrameHom.instFrameHomClass
infsInfHom 📖	CompOp	1 math math: infsInfHom_apply
instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass 📖	CompOp	—
instCoeTCFrameHomOfFrameHomClass 📖	CompOp	—
instCoeTCSInfHomOfSInfHomClass 📖	CompOp	—
instCoeTCSSupHomOfSSupHomClass 📖	CompOp	—
sInfHom 📖	CompData	30 math math: sInfHom.le_apply_bliminf, sSupHom.symm_dual_id, sInfHom.dual_id, LowerSet.coe_iicsInfHom, sInfHom.continuous, LowerSet.iicsInfHom_apply, sSupHom.dual_symm_apply_toFun, sInfHom.dual_apply_toFun, sInfHom.toFun_eq_coe, sSupHom.dual_apply_toFun, CompleteLatticeHom.coe_mk, sInfHom.coe_comp, sInfHom.coe_copy, infsInfHom_apply, sInfHom.coe_id, sSupHom.dual_comp, sInfHom.dual_comp, sInfHom.dual_symm_apply_toFun, sInfHom.id_apply, sInfHom.coe_top, CompleteLatticeHom.coe_tosInfHom, sInfHom.symm_dual_comp, sSupHom.symm_dual_comp, sInfHom.ext_iff, sInfHom.comp_apply, sSupHom.dual_id, sInfHom.instSInfHomClass, sInfHom.top_apply, sInfHom.coe_mk, sInfHom.symm_dual_id
sInfHomClass 📖	CompData	3 math math: OrderIsoClass.tosInfHomClass, sInfHom.instSInfHomClass, CompleteLatticeHomClass.tosInfHomClass
sSupHom 📖	CompData	30 math math: sSupHom.instSSupHomClass, CompleteLatticeHom.coe_tosSupHom, sSupHom.symm_dual_id, sInfHom.dual_id, sSupHom.coe_bot, sSupHom.bot_apply, sSupHom.dual_symm_apply_toFun, sInfHom.dual_apply_toFun, sSupHom.dual_apply_toFun, sSupHom.comp_apply, supsSupHom_apply, sSupHom.coe_id, UpperSet.coe_icisSupHom, sSupHom.continuous, sSupHom.toFun_eq_coe, sSupHom.dual_comp, sInfHom.dual_comp, sSupHom.coe_copy, UpperSet.icisSupHom_apply, sInfHom.dual_symm_apply_toFun, sSupHom.id_apply, sInfHom.symm_dual_comp, sSupHom.symm_dual_comp, sSupHom.setImage_toFun, sSupHom.ext_iff, sSupHom.apply_blimsup_le, sSupHom.dual_id, sSupHom.coe_mk, sSupHom.coe_comp, sInfHom.symm_dual_id
sSupHomClass 📖	CompData	4 math math: sSupHom.instSSupHomClass, OrderIsoClass.tosSupHomClass, FrameHomClass.tosSupHomClass, CompleteLatticeHomClass.tosSupHomClass
supsSupHom 📖	CompOp	1 math math: supsSupHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infsInfHom_apply 📖	mathematical	—	DFunLike.coe sInfHom Prod.infSet CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf sInfHom.instFunLike infsInfHom SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice	—	—
map_iInf 📖	mathematical	—	DFunLike.coe iInf	—	sInfHomClass.map_sInf Set.range_comp
map_iInf₂ 📖	mathematical	—	DFunLike.coe iInf	—	map_iInf
map_iSup 📖	mathematical	—	DFunLike.coe iSup	—	sSupHomClass.map_sSup
map_iSup₂ 📖	mathematical	—	DFunLike.coe iSup	—	map_iSup
supsSupHom_apply 📖	mathematical	—	DFunLike.coe sSupHom Prod.supSet CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup sSupHom.instFunLike supsSupHom SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice	—	—

sInfHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	11 math math: comp_id, id_comp, cancel_right, cancel_left, coe_comp, sSupHom.dual_comp, dual_comp, comp_assoc, symm_dual_comp, sSupHom.symm_dual_comp, comp_apply
copy 📖	CompOp	2 math math: copy_eq, coe_copy
dual 📖	CompOp	6 math math: dual_id, dual_apply_toFun, dual_comp, dual_symm_apply_toFun, symm_dual_comp, symm_dual_id
id 📖	CompOp	8 math math: sSupHom.symm_dual_id, dual_id, comp_id, id_comp, coe_id, id_apply, sSupHom.dual_id, symm_dual_id
instFunLike 📖	CompOp	20 math math: le_apply_bliminf, LowerSet.coe_iicsInfHom, continuous, LowerSet.iicsInfHom_apply, sSupHom.dual_symm_apply_toFun, dual_apply_toFun, toFun_eq_coe, CompleteLatticeHom.coe_mk, coe_comp, coe_copy, infsInfHom_apply, coe_id, id_apply, coe_top, CompleteLatticeHom.coe_tosInfHom, ext_iff, comp_apply, instSInfHomClass, top_apply, coe_mk
instInhabited 📖	CompOp	—
instOrderTop 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instTop 📖	CompOp	2 math math: coe_top, top_apply
toFun 📖	CompOp	9 math math: CompleteLatticeHom.dual_symm_apply_toFun, CompleteLatticeHom.toFun_eq_coe, CompleteLatticeHom.map_sSup', toFun_eq_coe, sSupHom.dual_apply_toFun, dual_symm_apply_toFun, CompleteLatticeHom.dual_apply_toFun, map_sInf', OrderIso.toCompleteLatticeHom_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe sInfHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe sInfHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe sInfHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe sInfHom instFunLike	DFunLike.coe sInfHom instFunLike copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe sInfHom instFunLike id	—	—
coe_mk 📖	mathematical	InfSet.sInf Set.image	DFunLike.coe sInfHom instFunLike	—	—
coe_top 📖	mathematical	—	DFunLike.coe sInfHom CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf instFunLike Top.top instTop Pi.instTopForall OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
comp_apply 📖	mathematical	—	DFunLike.coe sInfHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe sInfHom instFunLike	copy	—	DFunLike.ext'
dual_apply_toFun 📖	mathematical	—	DFunLike.coe sSupHom OrderDual OrderDual.supSet sSupHom.instFunLike Equiv sInfHom EquivLike.toFunLike Equiv.instEquivLike dual OrderDual.toDual instFunLike OrderDual.ofDual	—	—
dual_comp 📖	mathematical	—	DFunLike.coe Equiv sInfHom sSupHom OrderDual OrderDual.supSet EquivLike.toFunLike Equiv.instEquivLike dual comp sSupHom.comp	—	—
dual_id 📖	mathematical	—	DFunLike.coe Equiv sInfHom sSupHom OrderDual OrderDual.supSet EquivLike.toFunLike Equiv.instEquivLike dual id sSupHom.id	—	—
dual_symm_apply_toFun 📖	mathematical	—	toFun DFunLike.coe Equiv sSupHom OrderDual OrderDual.supSet sInfHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual OrderDual.ofDual sSupHom.instFunLike OrderDual.toDual	—	—
ext 📖	—	DFunLike.coe sInfHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe sInfHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe sInfHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instSInfHomClass 📖	mathematical	—	sInfHomClass sInfHom instFunLike	—	map_sInf'
map_sInf' 📖	mathematical	—	toFun InfSet.sInf Set.image	—	—
symm_dual_comp 📖	mathematical	—	DFunLike.coe Equiv sSupHom OrderDual OrderDual.supSet sInfHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual sSupHom.comp comp	—	—
symm_dual_id 📖	mathematical	—	DFunLike.coe Equiv sSupHom OrderDual OrderDual.supSet sInfHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual sSupHom.id id	—	—
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe sInfHom instFunLike	—	—
top_apply 📖	mathematical	—	DFunLike.coe sInfHom CompleteSemilatticeInf.toInfSet CompleteLattice.toCompleteSemilatticeInf instFunLike Top.top instTop OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

sInfHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_sInf 📖	mathematical	—	DFunLike.coe InfSet.sInf Set.image	—	—
toInfTopHomClass 📖	mathematical	—	InfTopHomClass SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	sInf_pair map_sInf Set.image_pair sInf_insert sInf_singleton sInf_empty Set.image_empty

sSupHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	11 math math: comp_apply, comp_id, cancel_left, dual_comp, sInfHom.dual_comp, cancel_right, sInfHom.symm_dual_comp, symm_dual_comp, id_comp, comp_assoc, coe_comp
copy 📖	CompOp	2 math math: copy_eq, coe_copy
dual 📖	CompOp	6 math math: symm_dual_id, dual_symm_apply_toFun, dual_apply_toFun, dual_comp, symm_dual_comp, dual_id
id 📖	CompOp	8 math math: symm_dual_id, sInfHom.dual_id, comp_id, coe_id, id_apply, id_comp, dual_id, sInfHom.symm_dual_id
instBot 📖	CompOp	2 math math: coe_bot, bot_apply
instFunLike 📖	CompOp	22 math math: instSSupHomClass, CompleteLatticeHom.coe_tosSupHom, coe_bot, bot_apply, dual_symm_apply_toFun, sInfHom.dual_apply_toFun, dual_apply_toFun, comp_apply, supsSupHom_apply, coe_id, UpperSet.coe_icisSupHom, continuous, toFun_eq_coe, coe_copy, UpperSet.icisSupHom_apply, sInfHom.dual_symm_apply_toFun, id_apply, setImage_toFun, ext_iff, apply_blimsup_le, coe_mk, coe_comp
instInhabited 📖	CompOp	—
instOrderBot 📖	CompOp	—
instPartialOrder 📖	CompOp	—
setImage 📖	CompOp	1 math math: setImage_toFun
toFun 📖	CompOp	2 math math: toFun_eq_coe, map_sSup'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_apply 📖	mathematical	—	DFunLike.coe sSupHom CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instFunLike Bot.bot instBot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
cancel_left 📖	mathematical	DFunLike.coe sSupHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe sSupHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_bot 📖	mathematical	—	DFunLike.coe sSupHom CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup instFunLike Bot.bot instBot Pi.instBotForall OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	—
coe_comp 📖	mathematical	—	DFunLike.coe sSupHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe sSupHom instFunLike	DFunLike.coe sSupHom instFunLike copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe sSupHom instFunLike id	—	—
coe_mk 📖	mathematical	SupSet.sSup Set.image	DFunLike.coe sSupHom instFunLike	—	—
comp_apply 📖	mathematical	—	DFunLike.coe sSupHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe sSupHom instFunLike	copy	—	DFunLike.ext'
dual_apply_toFun 📖	mathematical	—	sInfHom.toFun OrderDual OrderDual.infSet DFunLike.coe Equiv sSupHom sInfHom EquivLike.toFunLike Equiv.instEquivLike dual OrderDual.toDual instFunLike OrderDual.ofDual	—	—
dual_comp 📖	mathematical	—	DFunLike.coe Equiv sSupHom sInfHom OrderDual OrderDual.infSet EquivLike.toFunLike Equiv.instEquivLike dual comp sInfHom.comp	—	—
dual_id 📖	mathematical	—	DFunLike.coe Equiv sSupHom sInfHom OrderDual OrderDual.infSet EquivLike.toFunLike Equiv.instEquivLike dual id sInfHom.id	—	—
dual_symm_apply_toFun 📖	mathematical	—	DFunLike.coe sSupHom instFunLike Equiv sInfHom OrderDual OrderDual.infSet EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual OrderDual.ofDual sInfHom.instFunLike OrderDual.toDual	—	—
ext 📖	—	DFunLike.coe sSupHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe sSupHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe sSupHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instSSupHomClass 📖	mathematical	—	sSupHomClass sSupHom instFunLike	—	map_sSup'
map_sSup' 📖	mathematical	—	toFun SupSet.sSup Set.image	—	—
setImage_toFun 📖	mathematical	—	DFunLike.coe sSupHom Set Set.instSupSet instFunLike setImage Set.image	—	—
symm_dual_comp 📖	mathematical	—	DFunLike.coe Equiv sInfHom OrderDual OrderDual.infSet sSupHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual sInfHom.comp comp	—	—
symm_dual_id 📖	mathematical	—	DFunLike.coe Equiv sInfHom OrderDual OrderDual.infSet sSupHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm dual sInfHom.id id	—	—
toFun_eq_coe 📖	mathematical	—	toFun DFunLike.coe sSupHom instFunLike	—	—

sSupHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_sSup 📖	mathematical	—	DFunLike.coe SupSet.sSup Set.image	—	—
toSupBotHomClass 📖	mathematical	—	SupBotHomClass SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	sSup_pair map_sSup Set.image_pair sSup_insert sSup_singleton sSup_empty Set.image_empty

---

← Back to Index