Concept

📁 Source: Mathlib/Order/Concept.lean

Statistics

Metric	Count
Definitions Concept, copy, extent, instBoundedOrderConcept, instCompleteLattice, instInfSet, instInhabited, instLattice, instMax, instMin, instPartialOrder, instSemilatticeInf, instSemilatticeSup, instSupSet, intent, ofAttribute, ofAttributes, ofIsExtent, ofIsIntent, ofObject, ofObjects, swap, swapEquiv, IsExtent, IsIntent, extentClosure, intentClosure, lowerPolar, upperPolar	29
Theorems codisjoint_extent_intent, compl_extent, compl_intent, copy_eq, disjoint_extent_intent, ext, ext', ext_iff, extent_bot, extent_copy, extent_iInf, extent_iSup, extent_inf, extent_injective, extent_max, extent_min, extent_ofAttributes, extent_ofIsExtent, extent_ofIsIntent, extent_ofObjects, extent_ofObjects_of_isExtent, extent_sInf, extent_sSup, extent_ssubset_extent_iff, extent_subset_extent_iff, extent_sup, extent_swap, extent_top, intent_bot, intent_copy, intent_iInf, intent_iSup, intent_inf, intent_injective, intent_max, intent_min, intent_ofAttributes, intent_ofAttributes_of_isIntent, intent_ofIsExtent, intent_ofIsIntent, intent_ofObjects, intent_sInf, intent_sSup, intent_ssubset_intent_iff, intent_subset_intent_iff, intent_sup, intent_swap, intent_top, isCompl_extent_intent, isExtent_extent, isExtent_iff_exists_concept, isIntent_iff_exists_concept, isIntent_intent, isLowerSet_extent_le, isLowerSet_extent_lt, isUpperSet_intent_le, isUpperSet_intent_lt, le_ofAttributes_iff, le_ofObjects_of_extent_subset, leftInvOn_extent_ofObjects, leftInvOn_ofObjects_intent, leftInverse_ofAttributes_extent, leftInverse_ofObjects_extent, lowerPolar_intent, mem_extent_of_rel_extent, mem_intent_of_intent_rel, ofAttributes_intent, ofAttributes_le_of_intent_subset, ofObject_le_ofAttribute_iff, ofObjects_extent, ofObjects_le_iff, rel_extent_intent, strictAnti_intent, strictMono_extent, surjective_ofAttributes, surjective_ofObjects, swapEquiv_apply, swapEquiv_symm_apply, swap_le_swap_iff, swap_lt_swap_iff, swap_swap, upperPolar_extent, eq, iInter, iInter₂, inter, lowerPolar_upperPolar_subset, univ, eq, iInter, iInter₂, inter, univ, upperPolar_lowerPolar_subset, isExtent_iff, isExtent_lowerPolar, isIntent_iff, isIntent_upperPolar, extentClosure_apply, extentClosure_isClosed, gc_lowerPolar_upperPolar, gc_upperPolar_lowerPolar, intentClosure_apply, intentClosure_isClosed, lowerPolar_anti, lowerPolar_empty, lowerPolar_iUnion, lowerPolar_iUnion₂, lowerPolar_le, lowerPolar_swap, lowerPolar_union, lowerPolar_upperPolar_lowerPolar, lowerPolar_upperPolar_monotone, mem_lowerPolar_iff, mem_lowerPolar_singleton, mem_upperPolar_iff, mem_upperPolar_singleton, subset_lowerPolar_upperPolar, subset_upperPolar_iff_subset_lowerPolar, subset_upperPolar_lowerPolar, upperPolar_anti, upperPolar_empty, upperPolar_iUnion, upperPolar_iUnion₂, upperPolar_le, upperPolar_lowerPolar_monotone, upperPolar_lowerPolar_upperPolar, upperPolar_swap, upperPolar_union	129
Total	158

Concept

Definitions

Name	Category	Theorems
copy 📖	CompOp	3 math math: intent_copy, copy_eq, extent_copy
extent 📖	CompOp	43 math math: ofObjects_extent, lowerPolar_intent, extent_sSup, isLowerSet_extent_lt, extent_iInf, intent_iInf, intent_inf, mem_extent_of_rel_extent, isCompl_extent_intent, extent_ofIsExtent, extent_injective, extent_swap, compl_intent, ext_iff, extent_iSup, extent_ofObjects, extent_ofAttributes, extent_min, codisjoint_extent_intent, intent_swap, extent_subset_extent_iff, intent_min, isLowerSet_extent_le, intent_sInf, extent_sup, ofObjects_le_iff, isExtent_iff_exists_concept, extent_max, extent_top, extent_inf, extent_ofIsIntent, leftInvOn_extent_ofObjects, strictMono_extent, leftInverse_ofObjects_extent, extent_ofObjects_of_isExtent, extent_ssubset_extent_iff, compl_extent, upperPolar_extent, extent_bot, extent_sInf, isExtent_extent, disjoint_extent_intent, extent_copy
instBoundedOrderConcept 📖	CompOp	4 math math: intent_bot, intent_top, extent_top, extent_bot
instCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	4 math math: extent_iInf, intent_iInf, intent_sInf, extent_sInf
instInhabited 📖	CompOp	—
instLattice 📖	CompOp	—
instMax 📖	CompOp	4 math math: intent_max, intent_sup, extent_sup, extent_max
instMin 📖	CompOp	4 math math: intent_inf, extent_min, intent_min, extent_inf
instPartialOrder 📖	CompOp	29 math math: ofAttributes_le_of_intent_subset, intent_bot, DedekindCut.principalEmbedding_apply, DedekindCut.principalEmbedding_trans_factorEmbedding, intent_subset_intent_iff, DedekindCut.coe_principalEmbedding, DedekindCut.factorEmbedding_apply, swap_le_swap_iff, DedekindCut.principal_lt_principal, swapEquiv_apply, DedekindCut.principal_le_principal, intent_ssubset_intent_iff, extent_subset_extent_iff, DedekindCut.factorEmbedding_principal, ofObjects_le_iff, strictAnti_intent, le_ofAttributes_iff, swap_lt_swap_iff, DedekindCut.principalIso_apply, intent_top, DedekindCut.instTotalLe, ofObject_le_ofAttribute_iff, extent_top, strictMono_extent, le_ofObjects_of_extent_subset, swapEquiv_symm_apply, extent_ssubset_extent_iff, extent_bot, DedekindCut.principalIso_symm_apply
instSemilatticeInf 📖	CompOp	—
instSemilatticeSup 📖	CompOp	—
instSupSet 📖	CompOp	4 math math: extent_sSup, intent_sSup, intent_iSup, extent_iSup
intent 📖	CompOp	42 math math: intent_bot, intent_max, lowerPolar_intent, intent_ofIsExtent, extent_sSup, ofAttributes_intent, intent_sSup, intent_iInf, intent_inf, isCompl_extent_intent, intent_subset_intent_iff, isIntent_intent, intent_iSup, leftInvOn_ofObjects_intent, intent_ofObjects, extent_swap, compl_intent, extent_iSup, intent_copy, intent_ofAttributes_of_isIntent, codisjoint_extent_intent, intent_ofAttributes, intent_swap, intent_sup, intent_ssubset_intent_iff, isIntent_iff_exists_concept, intent_min, leftInverse_ofAttributes_extent, isUpperSet_intent_lt, isUpperSet_intent_le, intent_sInf, extent_sup, strictAnti_intent, extent_max, le_ofAttributes_iff, intent_top, mem_intent_of_intent_rel, intent_ofIsIntent, compl_extent, upperPolar_extent, intent_injective, disjoint_extent_intent
ofAttribute 📖	CompOp	2 math math: DedekindCut.ofAttribute_eq_principal, ofObject_le_ofAttribute_iff
ofAttributes 📖	CompOp	9 math math: ofAttributes_le_of_intent_subset, ofAttributes_intent, leftInvOn_ofObjects_intent, surjective_ofAttributes, extent_ofAttributes, intent_ofAttributes_of_isIntent, intent_ofAttributes, leftInverse_ofAttributes_extent, le_ofAttributes_iff
ofIsExtent 📖	CompOp	2 math math: intent_ofIsExtent, extent_ofIsExtent
ofIsIntent 📖	CompOp	2 math math: extent_ofIsIntent, intent_ofIsIntent
ofObject 📖	CompOp	2 math math: ofObject_le_ofAttribute_iff, DedekindCut.ofObject_eq_principal
ofObjects 📖	CompOp	9 math math: ofObjects_extent, intent_ofObjects, extent_ofObjects, surjective_ofObjects, ofObjects_le_iff, leftInvOn_extent_ofObjects, leftInverse_ofObjects_extent, le_ofObjects_of_extent_subset, extent_ofObjects_of_isExtent
swap 📖	CompOp	7 math math: swap_le_swap_iff, extent_swap, swap_swap, swapEquiv_apply, intent_swap, swap_lt_swap_iff, swapEquiv_symm_apply
swapEquiv 📖	CompOp	2 math math: swapEquiv_apply, swapEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_extent_intent 📖	mathematical	—	Codisjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop extent intent	—	codisjoint_iff_le_sup upperPolar_extent Not.imp_symm mem_extent_of_rel_extent
compl_extent 📖	mathematical	—	Compl.compl Set Set.instCompl extent intent	—	IsCompl.compl_eq isCompl_extent_intent
compl_intent 📖	mathematical	—	Compl.compl Set Set.instCompl intent extent	—	IsCompl.compl_eq IsCompl.symm isCompl_extent_intent
copy_eq 📖	mathematical	extent intent	copy	—	ext Set.ext copy.congr_simp
disjoint_extent_intent 📖	mathematical	—	Disjoint Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice extent intent	—	Set.disjoint_iff_forall_ne irrefl rel_extent_intent
ext 📖	—	extent	—	—	—
ext' 📖	—	intent	—	—	—
ext_iff 📖	mathematical	—	extent	—	ext
extent_bot 📖	mathematical	—	extent Bot.bot Concept OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderBot instBoundedOrderConcept lowerPolar Set.univ	—	—
extent_copy 📖	mathematical	extent intent	extent copy	—	—
extent_iInf 📖	mathematical	—	extent iInf Concept instInfSet Set.iInter	—	iInf_range
extent_iSup 📖	mathematical	—	extent iSup Concept instSupSet lowerPolar Set.iInter intent	—	iInf_range
extent_inf 📖	mathematical	—	extent Concept instMin Set Set.instInter	—	extent_min
extent_injective 📖	mathematical	—	Concept Set extent	—	ext
extent_max 📖	mathematical	—	extent Concept instMax lowerPolar Set Set.instInter intent	—	—
extent_min 📖	mathematical	—	extent Concept instMin Set Set.instInter	—	—
extent_ofAttributes 📖	mathematical	—	extent ofAttributes lowerPolar	—	—
extent_ofIsExtent 📖	mathematical	Order.IsExtent	extent ofIsExtent	—	—
extent_ofIsIntent 📖	mathematical	Order.IsIntent	extent ofIsIntent lowerPolar	—	—
extent_ofObjects 📖	mathematical	—	extent ofObjects lowerPolar upperPolar	—	—
extent_ofObjects_of_isExtent 📖	mathematical	Order.IsExtent	extent ofObjects	—	Order.IsExtent.eq
extent_sInf 📖	mathematical	—	extent InfSet.sInf Concept instInfSet Set.iInter Set Set.instMembership	—	—
extent_sSup 📖	mathematical	—	extent SupSet.sSup Concept instSupSet lowerPolar Set.iInter Set Set.instMembership intent	—	—
extent_ssubset_extent_iff 📖	mathematical	—	Set Set.instHasSSubset extent Concept Preorder.toLT PartialOrder.toPreorder instPartialOrder	—	—
extent_subset_extent_iff 📖	mathematical	—	Set Set.instHasSubset extent Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	—
extent_sup 📖	mathematical	—	extent Concept instMax lowerPolar Set Set.instInter intent	—	extent_max
extent_swap 📖	mathematical	—	extent Function.swap swap intent	—	—
extent_top 📖	mathematical	—	extent Top.top Concept OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderTop instBoundedOrderConcept Set.univ	—	—
intent_bot 📖	mathematical	—	intent Bot.bot Concept OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderBot instBoundedOrderConcept Set.univ	—	—
intent_copy 📖	mathematical	extent intent	intent copy	—	—
intent_iInf 📖	mathematical	—	intent iInf Concept instInfSet upperPolar Set.iInter extent	—	iInf_range
intent_iSup 📖	mathematical	—	intent iSup Concept instSupSet Set.iInter	—	iInf_range
intent_inf 📖	mathematical	—	intent Concept instMin upperPolar Set Set.instInter extent	—	intent_min
intent_injective 📖	mathematical	—	Concept Set intent	—	ext'
intent_max 📖	mathematical	—	intent Concept instMax Set Set.instInter	—	—
intent_min 📖	mathematical	—	intent Concept instMin upperPolar Set Set.instInter extent	—	—
intent_ofAttributes 📖	mathematical	—	intent ofAttributes upperPolar lowerPolar	—	—
intent_ofAttributes_of_isIntent 📖	mathematical	Order.IsIntent	intent ofAttributes	—	Order.IsIntent.eq
intent_ofIsExtent 📖	mathematical	Order.IsExtent	intent ofIsExtent upperPolar	—	—
intent_ofIsIntent 📖	mathematical	Order.IsIntent	intent ofIsIntent	—	—
intent_ofObjects 📖	mathematical	—	intent ofObjects upperPolar	—	—
intent_sInf 📖	mathematical	—	intent InfSet.sInf Concept instInfSet upperPolar Set.iInter Set Set.instMembership extent	—	—
intent_sSup 📖	mathematical	—	intent SupSet.sSup Concept instSupSet Set.iInter Set Set.instMembership	—	—
intent_ssubset_intent_iff 📖	mathematical	—	Set Set.instHasSSubset intent Concept Preorder.toLT PartialOrder.toPreorder instPartialOrder	—	ssubset_iff_subset_not_subset Set.instIsNonstrictStrictOrderSubsetSSubset lt_iff_le_not_ge intent_subset_intent_iff
intent_subset_intent_iff 📖	mathematical	—	Set Set.instHasSubset intent Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	extent_subset_extent_iff lowerPolar_intent lowerPolar_anti upperPolar_extent upperPolar_anti
intent_sup 📖	mathematical	—	intent Concept instMax Set Set.instInter	—	intent_max
intent_swap 📖	mathematical	—	intent Function.swap swap extent	—	—
intent_top 📖	mathematical	—	intent Top.top Concept OrderTop.toTop Preorder.toLE PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderTop instBoundedOrderConcept upperPolar Set.univ	—	—
isCompl_extent_intent 📖	mathematical	—	IsCompl Set CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instBoundedOrder extent intent	—	disjoint_extent_intent IsStrictOrder.toIrrefl IsStrictTotalOrder.toIsStrictOrder codisjoint_extent_intent IsStrictTotalOrder.toTrichotomous IsStrictOrder.toIsTrans
isExtent_extent 📖	mathematical	—	Order.IsExtent extent	—	Order.isExtent_lowerPolar lowerPolar_intent
isExtent_iff_exists_concept 📖	mathematical	—	Order.IsExtent Concept extent	—	isExtent_extent
isIntent_iff_exists_concept 📖	mathematical	—	Order.IsIntent Concept intent	—	isIntent_intent
isIntent_intent 📖	mathematical	—	Order.IsIntent intent	—	Order.isIntent_upperPolar upperPolar_extent
isLowerSet_extent_le 📖	mathematical	—	IsLowerSet Preorder.toLE extent	—	mem_extent_of_rel_extent instIsTransLe
isLowerSet_extent_lt 📖	mathematical	—	IsLowerSet Preorder.toLE PartialOrder.toPreorder extent Preorder.toLT	—	LE.le.eq_or_lt mem_extent_of_rel_extent instIsTransLt
isUpperSet_intent_le 📖	mathematical	—	IsUpperSet Preorder.toLE intent	—	mem_intent_of_intent_rel instIsTransLe
isUpperSet_intent_lt 📖	mathematical	—	IsUpperSet Preorder.toLE PartialOrder.toPreorder intent Preorder.toLT	—	LE.le.eq_or_lt mem_intent_of_intent_rel instIsTransLt
le_ofAttributes_iff 📖	mathematical	—	Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder ofAttributes Set Set.instHasSubset intent	—	intent_subset_intent_iff HasSubset.Subset.trans Set.instIsTransSubset subset_upperPolar_lowerPolar Order.IsIntent.upperPolar_lowerPolar_subset isIntent_intent
le_ofObjects_of_extent_subset 📖	mathematical	Set Set.instHasSubset extent	Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder ofObjects	—	upperPolar_extent lowerPolar_intent Antitone.comp lowerPolar_anti upperPolar_anti
leftInvOn_extent_ofObjects 📖	mathematical	—	Set.LeftInvOn Set Concept extent ofObjects setOf Order.IsExtent	—	Order.IsExtent.eq
leftInvOn_ofObjects_intent 📖	mathematical	—	Set.LeftInvOn Set Concept intent ofAttributes setOf Order.IsIntent	—	Order.IsIntent.eq
leftInverse_ofAttributes_extent 📖	mathematical	—	Concept Set ofAttributes intent	—	extent_injective lowerPolar_intent
leftInverse_ofObjects_extent 📖	mathematical	—	Concept Set ofObjects extent	—	ofObjects_extent
lowerPolar_intent 📖	mathematical	—	lowerPolar intent extent	—	—
mem_extent_of_rel_extent 📖	mathematical	Set Set.instMembership extent	Set Set.instMembership extent	—	lowerPolar_intent trans rel_extent_intent
mem_intent_of_intent_rel 📖	mathematical	Set Set.instMembership intent	Set Set.instMembership intent	—	upperPolar_extent trans rel_extent_intent
ofAttributes_intent 📖	mathematical	—	ofAttributes intent	—	extent_injective lowerPolar_intent
ofAttributes_le_of_intent_subset 📖	mathematical	Set Set.instHasSubset intent	Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder ofAttributes	—	intent_subset_intent_iff lowerPolar_intent upperPolar_extent Antitone.comp upperPolar_anti lowerPolar_anti
ofObject_le_ofAttribute_iff 📖	mathematical	—	Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder ofObject ofAttribute	—	—
ofObjects_extent 📖	mathematical	—	ofObjects extent	—	intent_injective upperPolar_extent
ofObjects_le_iff 📖	mathematical	—	Concept Preorder.toLE PartialOrder.toPreorder instPartialOrder ofObjects Set Set.instHasSubset extent	—	extent_subset_extent_iff HasSubset.Subset.trans Set.instIsTransSubset subset_lowerPolar_upperPolar Order.IsExtent.lowerPolar_upperPolar_subset isExtent_extent
rel_extent_intent 📖	—	Set Set.instMembership extent intent	—	—	upperPolar_extent
strictAnti_intent 📖	mathematical	—	StrictAnti Concept Set PartialOrder.toPreorder instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra intent	—	intent_ssubset_intent_iff
strictMono_extent 📖	mathematical	—	StrictMono Concept Set PartialOrder.toPreorder instPartialOrder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra extent	—	extent_ssubset_extent_iff
surjective_ofAttributes 📖	mathematical	—	Set Concept ofAttributes	—	Function.LeftInverse.surjective leftInverse_ofAttributes_extent
surjective_ofObjects 📖	mathematical	—	Set Concept ofObjects	—	Function.LeftInverse.surjective leftInverse_ofObjects_extent
swapEquiv_apply 📖	mathematical	—	DFunLike.coe RelIso OrderDual Concept Function.swap OrderDual.instLE Preorder.toLE PartialOrder.toPreorder instPartialOrder RelIso.instFunLike swapEquiv swap Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual	—	—
swapEquiv_symm_apply 📖	mathematical	—	DFunLike.coe RelIso Concept Function.swap OrderDual Preorder.toLE PartialOrder.toPreorder instPartialOrder OrderDual.instLE RelIso.instFunLike RelIso.symm swapEquiv Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual swap	—	—
swap_le_swap_iff 📖	mathematical	—	Concept Function.swap Preorder.toLE PartialOrder.toPreorder instPartialOrder swap	—	intent_subset_intent_iff
swap_lt_swap_iff 📖	mathematical	—	Concept Function.swap Preorder.toLT PartialOrder.toPreorder instPartialOrder swap	—	intent_ssubset_intent_iff
swap_swap 📖	mathematical	—	swap Function.swap	—	ext
upperPolar_extent 📖	mathematical	—	upperPolar extent intent	—	—

Order

Definitions

Name	Category	Theorems
IsExtent 📖	MathDef	9 math math: isExtent_iff, IsExtent.iInter₂, Concept.isExtent_iff_exists_concept, IsExtent.iInter, Concept.leftInvOn_extent_ofObjects, IsExtent.univ, isExtent_lowerPolar, Concept.isExtent_extent, IsExtent.inter
IsIntent 📖	MathDef	9 math math: IsIntent.iInter, IsIntent.inter, Concept.isIntent_intent, Concept.leftInvOn_ofObjects_intent, IsIntent.iInter₂, Concept.isIntent_iff_exists_concept, isIntent_iff, IsIntent.univ, isIntent_upperPolar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isExtent_iff 📖	mathematical	—	IsExtent lowerPolar upperPolar	—	lowerPolar_upperPolar_lowerPolar
isExtent_lowerPolar 📖	mathematical	—	IsExtent lowerPolar	—	—
isIntent_iff 📖	mathematical	—	IsIntent upperPolar lowerPolar	—	isExtent_iff
isIntent_upperPolar 📖	mathematical	—	IsIntent upperPolar	—	—

Order.IsExtent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	Order.IsExtent	lowerPolar upperPolar	—	Order.isExtent_iff
iInter 📖	mathematical	Order.IsExtent	Order.IsExtent Set.iInter	—	lowerPolar_iUnion Set.iInter_congr eq
iInter₂ 📖	mathematical	Order.IsExtent	Order.IsExtent Set.iInter	—	lowerPolar_iUnion₂ Set.iInter₂_congr eq
inter 📖	mathematical	Order.IsExtent	Order.IsExtent Set Set.instInter	—	lowerPolar_union
lowerPolar_upperPolar_subset 📖	mathematical	Order.IsExtent Set Set.instHasSubset	Set Set.instHasSubset lowerPolar upperPolar	—	eq lowerPolar_upperPolar_monotone
univ 📖	mathematical	—	Order.IsExtent Set.univ	—	Order.isExtent_iff GaloisConnection.u_l_top gc_upperPolar_lowerPolar

Order.IsIntent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	Order.IsIntent	upperPolar lowerPolar	—	Order.isIntent_iff
iInter 📖	mathematical	Order.IsIntent	Order.IsIntent Set.iInter	—	Order.IsExtent.iInter
iInter₂ 📖	mathematical	Order.IsIntent	Order.IsIntent Set.iInter	—	Order.IsExtent.iInter₂
inter 📖	mathematical	Order.IsIntent	Order.IsIntent Set Set.instInter	—	Order.IsExtent.inter
univ 📖	mathematical	—	Order.IsIntent Set.univ	—	Order.IsExtent.univ
upperPolar_lowerPolar_subset 📖	mathematical	Order.IsIntent Set Set.instHasSubset	Set Set.instHasSubset upperPolar lowerPolar	—	eq upperPolar_lowerPolar_monotone

(root)

Definitions

Name	Category	Theorems
Concept 📖	CompData	45 math math: Concept.ofAttributes_le_of_intent_subset, Concept.intent_bot, Concept.intent_max, Concept.extent_sSup, Concept.extent_iInf, Concept.intent_sSup, Concept.intent_iInf, Concept.intent_inf, Concept.intent_subset_intent_iff, Concept.intent_iSup, Concept.leftInvOn_ofObjects_intent, Concept.swap_le_swap_iff, Concept.extent_injective, Concept.extent_iSup, Concept.swapEquiv_apply, Concept.surjective_ofAttributes, Concept.extent_min, Concept.intent_sup, Concept.intent_ssubset_intent_iff, Concept.extent_subset_extent_iff, Concept.isIntent_iff_exists_concept, Concept.intent_min, Concept.leftInverse_ofAttributes_extent, Concept.intent_sInf, Concept.surjective_ofObjects, Concept.extent_sup, Concept.ofObjects_le_iff, Concept.strictAnti_intent, Concept.isExtent_iff_exists_concept, Concept.extent_max, Concept.le_ofAttributes_iff, Concept.swap_lt_swap_iff, Concept.intent_top, Concept.ofObject_le_ofAttribute_iff, Concept.extent_top, Concept.extent_inf, Concept.leftInvOn_extent_ofObjects, Concept.strictMono_extent, Concept.leftInverse_ofObjects_extent, Concept.le_ofObjects_of_extent_subset, Concept.swapEquiv_symm_apply, Concept.extent_ssubset_extent_iff, Concept.extent_bot, Concept.extent_sInf, Concept.intent_injective
extentClosure 📖	CompOp	2 math math: extentClosure_apply, extentClosure_isClosed
intentClosure 📖	CompOp	2 math math: intentClosure_isClosed, intentClosure_apply
lowerPolar 📖	CompOp	40 math math: lowerPolar_swap, lowerPolar_union, Order.IsExtent.eq, Concept.lowerPolar_intent, Order.isExtent_iff, Concept.extent_sSup, lowerPolar_anti, extentClosure_apply, lowerPolar_iUnion₂, subset_upperPolar_lowerPolar, gc_upperPolar_lowerPolar, lowerPolar_empty, mem_lowerPolar_singleton, subset_lowerPolar_upperPolar, Order.IsExtent.lowerPolar_upperPolar_subset, upperPolar_lowerPolar_upperPolar, lowerPolar_upperPolar_monotone, Concept.extent_iSup, Concept.extent_ofObjects, Concept.extent_ofAttributes, Concept.intent_ofAttributes, lowerPolar_iUnion, intentClosure_isClosed, Order.isIntent_iff, Concept.extent_sup, intentClosure_apply, lowerPolar_le, Concept.extent_max, Order.IsIntent.eq, Concept.extent_ofIsIntent, lowerPolar_upperPolar_lowerPolar, upperPolar_swap, extentClosure_isClosed, upperPolar_lowerPolar_monotone, Concept.extent_bot, Order.isExtent_lowerPolar, Order.IsIntent.upperPolar_lowerPolar_subset, gc_lowerPolar_upperPolar, mem_lowerPolar_iff, subset_upperPolar_iff_subset_lowerPolar
upperPolar 📖	CompOp	40 math math: lowerPolar_swap, Order.IsExtent.eq, Concept.intent_ofIsExtent, Order.isExtent_iff, mem_upperPolar_iff, extentClosure_apply, mem_upperPolar_singleton, subset_upperPolar_lowerPolar, Concept.intent_iInf, Concept.intent_inf, gc_upperPolar_lowerPolar, upperPolar_union, upperPolar_empty, subset_lowerPolar_upperPolar, Concept.intent_ofObjects, Order.IsExtent.lowerPolar_upperPolar_subset, upperPolar_lowerPolar_upperPolar, lowerPolar_upperPolar_monotone, Concept.extent_ofObjects, upperPolar_le, Concept.intent_ofAttributes, intentClosure_isClosed, Concept.intent_min, Order.isIntent_iff, Concept.intent_sInf, intentClosure_apply, upperPolar_iUnion₂, Concept.intent_top, Order.IsIntent.eq, Order.isIntent_upperPolar, lowerPolar_upperPolar_lowerPolar, upperPolar_anti, upperPolar_swap, extentClosure_isClosed, Concept.upperPolar_extent, upperPolar_lowerPolar_monotone, Order.IsIntent.upperPolar_lowerPolar_subset, gc_lowerPolar_upperPolar, subset_upperPolar_iff_subset_lowerPolar, upperPolar_iUnion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extentClosure_apply 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike extentClosure lowerPolar upperPolar	—	—
extentClosure_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra extentClosure lowerPolar upperPolar	—	—
gc_lowerPolar_upperPolar 📖	mathematical	—	GaloisConnection Set OrderDual PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual lowerPolar upperPolar OrderDual.ofDual	—	subset_upperPolar_iff_subset_lowerPolar
gc_upperPolar_lowerPolar 📖	mathematical	—	GaloisConnection Set OrderDual PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual upperPolar lowerPolar OrderDual.ofDual	—	subset_upperPolar_iff_subset_lowerPolar
intentClosure_apply 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike intentClosure upperPolar lowerPolar	—	—
intentClosure_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra intentClosure upperPolar lowerPolar	—	—
lowerPolar_anti 📖	mathematical	—	Antitone Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra lowerPolar	—	upperPolar_anti
lowerPolar_empty 📖	mathematical	—	lowerPolar Set Set.instEmptyCollection Set.univ	—	upperPolar_empty
lowerPolar_iUnion 📖	mathematical	—	lowerPolar Set.iUnion Set.iInter	—	upperPolar_iUnion
lowerPolar_iUnion₂ 📖	mathematical	—	lowerPolar Set.iUnion Set.iInter	—	upperPolar_iUnion₂
lowerPolar_le 📖	mathematical	—	lowerPolar lowerBounds	—	—
lowerPolar_swap 📖	mathematical	—	lowerPolar Function.swap upperPolar	—	—
lowerPolar_union 📖	mathematical	—	lowerPolar Set Set.instUnion Set.instInter	—	upperPolar_union
lowerPolar_upperPolar_lowerPolar 📖	mathematical	—	lowerPolar upperPolar	—	upperPolar_lowerPolar_upperPolar
lowerPolar_upperPolar_monotone 📖	mathematical	—	Monotone Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra lowerPolar upperPolar	—	GaloisConnection.monotone_u_comp_l gc_upperPolar_lowerPolar
mem_lowerPolar_iff 📖	mathematical	—	Set Set.instMembership lowerPolar	—	—
mem_lowerPolar_singleton 📖	mathematical	—	Set Set.instMembership lowerPolar Set.instSingletonSet	—	—
mem_upperPolar_iff 📖	mathematical	—	Set Set.instMembership upperPolar	—	—
mem_upperPolar_singleton 📖	mathematical	—	Set Set.instMembership upperPolar Set.instSingletonSet	—	—
subset_lowerPolar_upperPolar 📖	mathematical	—	Set Set.instHasSubset lowerPolar upperPolar	—	GaloisConnection.le_u_l gc_upperPolar_lowerPolar
subset_upperPolar_iff_subset_lowerPolar 📖	mathematical	—	Set Set.instHasSubset upperPolar lowerPolar	—	—
subset_upperPolar_lowerPolar 📖	mathematical	—	Set Set.instHasSubset upperPolar lowerPolar	—	subset_lowerPolar_upperPolar
upperPolar_anti 📖	mathematical	—	Antitone Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra upperPolar	—	GaloisConnection.monotone_l gc_upperPolar_lowerPolar
upperPolar_empty 📖	mathematical	—	upperPolar Set Set.instEmptyCollection Set.univ	—	Set.eq_univ_of_forall
upperPolar_iUnion 📖	mathematical	—	upperPolar Set.iUnion Set.iInter	—	GaloisConnection.l_iSup gc_upperPolar_lowerPolar
upperPolar_iUnion₂ 📖	mathematical	—	upperPolar Set.iUnion Set.iInter	—	GaloisConnection.l_iSup₂ gc_upperPolar_lowerPolar
upperPolar_le 📖	mathematical	—	upperPolar upperBounds	—	—
upperPolar_lowerPolar_monotone 📖	mathematical	—	Monotone Set PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra upperPolar lowerPolar	—	GaloisConnection.monotone_u_comp_l gc_lowerPolar_upperPolar
upperPolar_lowerPolar_upperPolar 📖	mathematical	—	upperPolar lowerPolar	—	GaloisConnection.l_u_l_eq_l gc_upperPolar_lowerPolar
upperPolar_swap 📖	mathematical	—	upperPolar Function.swap lowerPolar	—	—
upperPolar_union 📖	mathematical	—	upperPolar Set Set.instUnion Set.instInter	—	Set.ext forall₂_or_left

---

← Back to Index