SetLike

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

Statistics

Metric	Count
Definitions	0
Theorems ext, ext_iff, mem_iInf, mem_iSup, mem_inf, mem_sInf, mem_sSup, mem_subtype, mem_sup, mem_top, notMem_bot, ext_mem, ext_mem_iff, mem_subtype, setLike_mem_coe, setLike_mem_inf, setLike_mem_sup	17
Total	17

CompleteSublattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet	—	ext
mem_iInf 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet iInf instInfSet	—	map_iInf CompleteLatticeHomClass.tosInfHomClass CompleteLatticeHom.instCompleteLatticeHomClass
mem_iSup 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet iSup instSupSet	—	map_iSup FrameHomClass.tosSupHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass
mem_inf 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet instMinSubtypeMem	—	InfHomClass.map_inf InfTopHomClass.toInfHomClass FrameHomClass.toInfTopHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass
mem_sInf 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet InfSet.sInf instInfSet	—	sInfHomClass.map_sInf CompleteLatticeHomClass.tosInfHomClass CompleteLatticeHom.instCompleteLatticeHomClass Set.image_congr Set.sInter_image
mem_sSup 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet SupSet.sSup instSupSet Set.instMembership	—	sSupHomClass.map_sSup FrameHomClass.tosSupHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass Set.image_congr Set.sUnion_image
mem_subtype 📖	mathematical	—	Set Set.instMembership DFunLike.coe CompleteLatticeHom CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike instCompleteLattice CompleteLatticeHom.instFunLike subtype SetLike.instSubtypeSet	—	—
mem_sup 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet instMaxSubtypeMem	—	SupHomClass.map_sup SupBotHomClass.toSupHomClass sSupHomClass.toSupBotHomClass FrameHomClass.tosSupHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass
mem_top 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet Top.top instTop	—	TopHomClass.map_top InfTopHomClass.toTopHomClass FrameHomClass.toInfTopHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass
notMem_bot 📖	mathematical	—	Set CompleteSublattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet Bot.bot instBot	—	BotHomClass.map_bot SupBotHomClass.toBotHomClass sSupHomClass.toSupBotHomClass FrameHomClass.tosSupHomClass CompleteLatticeHomClass.toFrameHomClass CompleteLatticeHom.instCompleteLatticeHomClass

Sublattice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_mem 📖	—	Set Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet	—	—	SetLike.ext
ext_mem_iff 📖	mathematical	—	Set Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet	—	ext_mem
mem_subtype 📖	mathematical	—	Set Set.instMembership DFunLike.coe LatticeHom Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike instLatticeCoe LatticeHom.instFunLike subtype SetLike.instSubtypeSet	—	—
setLike_mem_coe 📖	mathematical	—	Set Set.instMembership Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet	—	—
setLike_mem_inf 📖	mathematical	—	Set Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet instInfCoe	—	InfHomClass.map_inf LatticeHomClass.toInfHomClass LatticeHom.instLatticeHomClass
setLike_mem_sup 📖	mathematical	—	Set Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra SetLike.instMembership instSetLike SetLike.instSubtypeSet instSupCoe	—	SupHomClass.map_sup LatticeHomClass.toSupHomClass LatticeHom.instLatticeHomClass

---

← Back to Index