Hom

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

Statistics

Metric	Count
Definitions BiheytingHom, comp, copy, id, instFunLike, instInhabited, instPartialOrder, toLatticeHom, BiheytingHomClass, CoheytingHom, comp, copy, id, instFunLike, instInhabited, instPartialOrder, toLatticeHom, CoheytingHomClass, HeytingHom, comp, copy, id, instFunLike, instInhabited, instPartialOrder, toLatticeHom, HeytingHomClass, instCoeTCBiheytingHomOfBiheytingHomClass, instCoeTCCoheytingHomOfCoheytingHomClass, instCoeTCHeytingHomOfHeytingHomClass	30
Theorems cancel_left, cancel_right, coe_comp, coe_copy, coe_id, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instBiheytingHomClass, map_himp', map_sdiff', toFun_eq_coe, toFun_eq_coe_aux, map_himp, map_sdiff, toCoheytingHomClass, toHeytingHomClass, toLatticeHomClass, toBiheytingHomClass, cancel_left, cancel_right, coe_comp, coe_copy, coe_id, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instCoheytingHomClass, map_sdiff', map_top', toFun_eq_coe, toFun_eq_coe_aux, map_sdiff, map_top, toBoundedLatticeHomClass, toLatticeHomClass, cancel_left, cancel_right, coe_comp, coe_copy, coe_id, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instHeytingHomClass, map_bot', map_himp', toFun_eq_coe, toFun_eq_coe_aux, map_bot, map_himp, toBoundedLatticeHomClass, toLatticeHomClass, toBiheytingHomClass, toCoheytingHomClass, toHeytingHomClass, map_bihimp, map_compl, map_hnot, map_symmDiff	75
Total	105

BiheytingHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	7 math math: cancel_left, comp_assoc, id_comp, comp_id, cancel_right, coe_comp, comp_apply
copy 📖	CompOp	2 math math: coe_copy, copy_eq
id 📖	CompOp	4 math math: id_comp, coe_id, id_apply, comp_id
instFunLike 📖	CompOp	8 math math: instBiheytingHomClass, toFun_eq_coe_aux, coe_id, toFun_eq_coe, ext_iff, id_apply, coe_comp, comp_apply
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	—
toLatticeHom 📖	CompOp	4 math math: map_sdiff', toFun_eq_coe_aux, toFun_eq_coe, map_himp'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe BiheytingHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe BiheytingHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe BiheytingHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe BiheytingHom instFunLike	copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe BiheytingHom instFunLike id	—	—
comp_apply 📖	mathematical	—	DFunLike.coe BiheytingHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe BiheytingHom instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe BiheytingHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe BiheytingHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe BiheytingHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instBiheytingHomClass 📖	mathematical	—	BiheytingHomClass BiheytingHom instFunLike	—	SupHom.map_sup' LatticeHom.map_inf' map_himp' map_sdiff'
map_himp' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra LatticeHom.toSupHom toLatticeHom HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra BiheytingAlgebra.toHeytingAlgebra	—	—
map_sdiff' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra LatticeHom.toSupHom toLatticeHom BiheytingAlgebra.toSDiff	—	—
toFun_eq_coe 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra LatticeHom.toSupHom toLatticeHom DFunLike.coe BiheytingHom instFunLike	—	—
toFun_eq_coe_aux 📖	mathematical	—	DFunLike.coe LatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra LatticeHom.instFunLike toLatticeHom BiheytingHom instFunLike	—	—

BiheytingHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_himp 📖	mathematical	—	DFunLike.coe HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra BiheytingAlgebra.toHeytingAlgebra	—	—
map_sdiff 📖	mathematical	—	DFunLike.coe BiheytingAlgebra.toSDiff	—	—
toCoheytingHomClass 📖	mathematical	—	CoheytingHomClass BiheytingAlgebra.toCoheytingAlgebra	—	toLatticeHomClass himp_self map_himp map_sdiff
toHeytingHomClass 📖	mathematical	—	HeytingHomClass BiheytingAlgebra.toHeytingAlgebra	—	toLatticeHomClass sdiff_self map_sdiff map_himp
toLatticeHomClass 📖	mathematical	—	LatticeHomClass GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra	—	—

BoundedLatticeHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBiheytingHomClass 📖	mathematical	—	BiheytingHomClass BooleanAlgebra.toBiheytingAlgebra	—	toLatticeHomClass himp_eq SupHomClass.map_sup SupBotHomClass.toSupHomClass toSupBotHomClass IsCompl.compl_eq IsCompl.map isCompl_compl sdiff_eq InfHomClass.map_inf InfTopHomClass.toInfHomClass toInfTopHomClass

CoheytingHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	7 math math: id_comp, comp_apply, comp_assoc, comp_id, cancel_left, cancel_right, coe_comp
copy 📖	CompOp	2 math math: copy_eq, coe_copy
id 📖	CompOp	4 math math: id_apply, id_comp, coe_id, comp_id
instFunLike 📖	CompOp	8 math math: id_apply, toFun_eq_coe_aux, coe_id, comp_apply, toFun_eq_coe, coe_comp, instCoheytingHomClass, ext_iff
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	—
toLatticeHom 📖	CompOp	4 math math: toFun_eq_coe_aux, map_top', map_sdiff', toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe CoheytingHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe CoheytingHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe CoheytingHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe CoheytingHom instFunLike	copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe CoheytingHom instFunLike id	—	—
comp_apply 📖	mathematical	—	DFunLike.coe CoheytingHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe CoheytingHom instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe CoheytingHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe CoheytingHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe CoheytingHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instCoheytingHomClass 📖	mathematical	—	CoheytingHomClass CoheytingHom instFunLike	—	SupHom.map_sup' LatticeHom.map_inf' map_top' map_sdiff'
map_sdiff' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra LatticeHom.toSupHom toLatticeHom GeneralizedCoheytingAlgebra.toSDiff	—	—
map_top' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra LatticeHom.toSupHom toLatticeHom Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder CoheytingAlgebra.toOrderTop	—	—
toFun_eq_coe 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra LatticeHom.toSupHom toLatticeHom DFunLike.coe CoheytingHom instFunLike	—	—
toFun_eq_coe_aux 📖	mathematical	—	DFunLike.coe LatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra LatticeHom.instFunLike toLatticeHom CoheytingHom instFunLike	—	—

CoheytingHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_sdiff 📖	mathematical	—	DFunLike.coe GeneralizedCoheytingAlgebra.toSDiff CoheytingAlgebra.toGeneralizedCoheytingAlgebra	—	—
map_top 📖	mathematical	—	DFunLike.coe Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toOrderTop	—	—
toBoundedLatticeHomClass 📖	mathematical	—	BoundedLatticeHomClass GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra CoheytingAlgebra.toBoundedOrder	—	toLatticeHomClass map_top sdiff_self map_sdiff
toLatticeHomClass 📖	mathematical	—	LatticeHomClass GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra	—	—

HeytingHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	9 math math: HeytAlg.hom_comp, coe_comp, cancel_right, id_comp, cancel_left, comp_id, comp_assoc, HeytAlg.ofHom_comp, comp_apply
copy 📖	CompOp	2 math math: copy_eq, coe_copy
id 📖	CompOp	6 math math: HeytAlg.hom_id, id_comp, HeytAlg.ofHom_id, comp_id, coe_id, id_apply
instFunLike 📖	CompOp	23 math math: HeytAlg.hasForgetToLat_forget₂_map, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, HeytAlg.coe_comp, coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, HeytAlg.id_apply, HeytAlg.hom_inv_apply, HeytAlg.inv_hom_apply, HeytAlg.comp_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, toFun_eq_coe_aux, HeytAlg.ofHom_apply, HeytAlg.coe_id, instHeytingHomClass, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, toFun_eq_coe, comp_apply, HeytAlg.forget_map, HeytAlg.ext_iff, coe_id, ext_iff, id_apply
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	—
toLatticeHom 📖	CompOp	4 math math: map_himp', toFun_eq_coe_aux, map_bot', toFun_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe HeytingHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe HeytingHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe HeytingHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe HeytingHom instFunLike	copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe HeytingHom instFunLike id	—	—
comp_apply 📖	mathematical	—	DFunLike.coe HeytingHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe HeytingHom instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe HeytingHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe HeytingHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe HeytingHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instHeytingHomClass 📖	mathematical	—	HeytingHomClass HeytingHom instFunLike	—	SupHom.map_sup' LatticeHom.map_inf' map_bot' map_himp'
map_bot' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra LatticeHom.toSupHom toLatticeHom Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder HeytingAlgebra.toOrderBot	—	—
map_himp' 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra LatticeHom.toSupHom toLatticeHom HImp.himp GeneralizedHeytingAlgebra.toHImp	—	—
toFun_eq_coe 📖	mathematical	—	SupHom.toFun SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra LatticeHom.toSupHom toLatticeHom DFunLike.coe HeytingHom instFunLike	—	—
toFun_eq_coe_aux 📖	mathematical	—	DFunLike.coe LatticeHom GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra LatticeHom.instFunLike toLatticeHom HeytingHom instFunLike	—	—

HeytingHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_bot 📖	mathematical	—	DFunLike.coe Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toOrderBot	—	—
map_himp 📖	mathematical	—	DFunLike.coe HImp.himp GeneralizedHeytingAlgebra.toHImp HeytingAlgebra.toGeneralizedHeytingAlgebra	—	—
toBoundedLatticeHomClass 📖	mathematical	—	BoundedLatticeHomClass GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toBoundedOrder	—	toLatticeHomClass himp_self map_himp map_bot
toLatticeHomClass 📖	mathematical	—	LatticeHomClass GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	—	—

OrderIsoClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toBiheytingHomClass 📖	mathematical	—	BiheytingHomClass EquivLike.toFunLike	—	toLatticeHomClass eq_of_forall_le_iff map_le_map_iff InfHomClass.map_inf InfTopHomClass.toInfHomClass toInfTopHomClass EquivLike.apply_inv_apply eq_of_forall_ge_iff SupHomClass.map_sup SupBotHomClass.toSupHomClass toSupBotHomClass
toCoheytingHomClass 📖	mathematical	—	CoheytingHomClass EquivLike.toFunLike	—	toBoundedLatticeHomClass BoundedLatticeHomClass.toLatticeHomClass BoundedLatticeHomClass.map_top eq_of_forall_ge_iff map_le_map_iff SupHomClass.map_sup SupBotHomClass.toSupHomClass toSupBotHomClass EquivLike.apply_inv_apply
toHeytingHomClass 📖	mathematical	—	HeytingHomClass EquivLike.toFunLike	—	toBoundedLatticeHomClass BoundedLatticeHomClass.toLatticeHomClass BoundedLatticeHomClass.map_bot eq_of_forall_le_iff map_le_map_iff InfHomClass.map_inf InfTopHomClass.toInfHomClass toInfTopHomClass EquivLike.apply_inv_apply

(root)

Definitions

Name	Category	Theorems
BiheytingHom 📖	CompData	8 math math: BiheytingHom.instBiheytingHomClass, BiheytingHom.toFun_eq_coe_aux, BiheytingHom.coe_id, BiheytingHom.toFun_eq_coe, BiheytingHom.ext_iff, BiheytingHom.id_apply, BiheytingHom.coe_comp, BiheytingHom.comp_apply
BiheytingHomClass 📖	CompData	3 math math: BiheytingHom.instBiheytingHomClass, OrderIsoClass.toBiheytingHomClass, BoundedLatticeHomClass.toBiheytingHomClass
CoheytingHom 📖	CompData	8 math math: CoheytingHom.id_apply, CoheytingHom.toFun_eq_coe_aux, CoheytingHom.coe_id, CoheytingHom.comp_apply, CoheytingHom.toFun_eq_coe, CoheytingHom.coe_comp, CoheytingHom.instCoheytingHomClass, CoheytingHom.ext_iff
CoheytingHomClass 📖	CompData	3 math math: BiheytingHomClass.toCoheytingHomClass, CoheytingHom.instCoheytingHomClass, OrderIsoClass.toCoheytingHomClass
HeytingHom 📖	CompData	23 math math: HeytAlg.hasForgetToLat_forget₂_map, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, HeytAlg.coe_comp, HeytingHom.coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, HeytAlg.id_apply, HeytAlg.hom_inv_apply, HeytAlg.inv_hom_apply, HeytAlg.comp_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, HeytingHom.toFun_eq_coe_aux, HeytAlg.ofHom_apply, HeytAlg.coe_id, HeytingHom.instHeytingHomClass, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, HeytingHom.toFun_eq_coe, HeytingHom.comp_apply, HeytAlg.forget_map, HeytAlg.ext_iff, HeytingHom.coe_id, HeytingHom.ext_iff, HeytingHom.id_apply
HeytingHomClass 📖	CompData	3 math math: BiheytingHomClass.toHeytingHomClass, OrderIsoClass.toHeytingHomClass, HeytingHom.instHeytingHomClass
instCoeTCBiheytingHomOfBiheytingHomClass 📖	CompOp	—
instCoeTCCoheytingHomOfCoheytingHomClass 📖	CompOp	—
instCoeTCHeytingHomOfHeytingHomClass 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_bihimp 📖	mathematical	—	DFunLike.coe bihimp SemilatticeInf.toMin Lattice.toSemilatticeInf GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra GeneralizedHeytingAlgebra.toHImp	—	InfHomClass.map_inf InfTopHomClass.toInfHomClass BoundedLatticeHomClass.toInfTopHomClass HeytingHomClass.toBoundedLatticeHomClass HeytingHomClass.map_himp
map_compl 📖	mathematical	—	DFunLike.coe Compl.compl HeytingAlgebra.toCompl	—	himp_bot HeytingHomClass.map_himp BotHomClass.map_bot SupBotHomClass.toBotHomClass BoundedLatticeHomClass.toSupBotHomClass HeytingHomClass.toBoundedLatticeHomClass
map_hnot 📖	mathematical	—	DFunLike.coe HNot.hnot CoheytingAlgebra.toHNot	—	top_sdiff' CoheytingHomClass.map_sdiff TopHomClass.map_top InfTopHomClass.toTopHomClass BoundedLatticeHomClass.toInfTopHomClass CoheytingHomClass.toBoundedLatticeHomClass
map_symmDiff 📖	mathematical	—	DFunLike.coe symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra GeneralizedCoheytingAlgebra.toSDiff	—	SupHomClass.map_sup SupBotHomClass.toSupHomClass BoundedLatticeHomClass.toSupBotHomClass CoheytingHomClass.toBoundedLatticeHomClass CoheytingHomClass.map_sdiff

---

← Back to Index