Concept

📁 Source: Mathlib/Order/Concept.lean

Statistics

Metric	Count
Definitions Concept, copy, extent, instBoundedOrderConcept, instCompleteLattice, instInfConcept, instInfSet, instInhabited, instLatticeConcept, instPartialOrder, instSemilatticeInfConcept, instSupConcept, instSupSet, intent, swap, swapEquiv, lowerPolar, upperPolar	18
Theorems codisjoint_extent_intent, compl_extent, compl_intent, copy_eq, copy_extent, copy_intent, disjoint_extent_intent, ext, ext', ext_iff, extent_bot, extent_iInf, extent_iSup, extent_inf, extent_injective, extent_sInf, extent_sSup, extent_ssubset_extent_iff, extent_subset_extent_iff, extent_sup, extent_top, intent_bot, intent_iInf, intent_iSup, intent_inf, intent_injective, intent_sInf, intent_sSup, intent_ssubset_intent_iff, intent_subset_intent_iff, intent_sup, intent_top, isCompl_extent_intent, lowerPolar_intent, mem_extent_of_rel_extent, mem_intent_of_intent_rel, rel_extent_intent, strictAnti_intent, strictMono_extent, swapEquiv_apply, swapEquiv_symm_apply, swap_extent, swap_intent, swap_le_swap_iff, swap_lt_swap_iff, swap_swap, upperPolar_extent, gc_upperPolar_lowerPolar, lowerPolar_anti, lowerPolar_empty, lowerPolar_iUnion, lowerPolar_iUnion₂, lowerPolar_swap, lowerPolar_union, lowerPolar_upperPolar_lowerPolar, subset_lowerPolar_upperPolar, subset_upperPolar_iff_subset_lowerPolar, subset_upperPolar_lowerPolar, upperPolar_anti, upperPolar_empty, upperPolar_iUnion, upperPolar_iUnion₂, upperPolar_lowerPolar_upperPolar, upperPolar_swap, upperPolar_union	65
Total	83

Concept

Definitions

Name	Category	Theorems
copy 📖	CompOp	3 math math: copy_extent, copy_eq, copy_intent
extent 📖	CompOp	25 math math: lowerPolar_intent, extent_sSup, swap_intent, extent_iInf, intent_iInf, intent_inf, isCompl_extent_intent, swap_extent, extent_injective, compl_intent, ext_iff, extent_iSup, codisjoint_extent_intent, extent_subset_extent_iff, intent_sInf, extent_sup, extent_top, extent_inf, strictMono_extent, extent_ssubset_extent_iff, compl_extent, upperPolar_extent, extent_bot, extent_sInf, disjoint_extent_intent
instBoundedOrderConcept 📖	CompOp	4 math math: intent_bot, intent_top, extent_top, extent_bot
instCompleteLattice 📖	CompOp	—
instInfConcept 📖	CompOp	2 math math: intent_inf, extent_inf
instInfSet 📖	CompOp	4 math math: extent_iInf, intent_iInf, intent_sInf, extent_sInf
instInhabited 📖	CompOp	—
instLatticeConcept 📖	CompOp	—
instPartialOrder 📖	CompOp	14 math math: intent_bot, intent_subset_intent_iff, swap_le_swap_iff, swapEquiv_apply, intent_ssubset_intent_iff, extent_subset_extent_iff, strictAnti_intent, swap_lt_swap_iff, intent_top, extent_top, strictMono_extent, swapEquiv_symm_apply, extent_ssubset_extent_iff, extent_bot
instSemilatticeInfConcept 📖	CompOp	—
instSupConcept 📖	CompOp	2 math math: intent_sup, extent_sup
instSupSet 📖	CompOp	4 math math: extent_sSup, intent_sSup, intent_iSup, extent_iSup
intent 📖	CompOp	24 math math: intent_bot, lowerPolar_intent, extent_sSup, swap_intent, intent_sSup, intent_iInf, intent_inf, isCompl_extent_intent, intent_subset_intent_iff, intent_iSup, swap_extent, compl_intent, extent_iSup, codisjoint_extent_intent, intent_sup, intent_ssubset_intent_iff, intent_sInf, extent_sup, strictAnti_intent, intent_top, compl_extent, upperPolar_extent, intent_injective, disjoint_extent_intent
swap 📖	CompOp	7 math math: swap_intent, swap_le_swap_iff, swap_extent, swap_swap, swapEquiv_apply, 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
copy_extent 📖	mathematical	extent intent	copy	—	—
copy_intent 📖	mathematical	extent intent	copy	—	—
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_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 instInfConcept Set Set.instInter	—	—
extent_injective 📖	mathematical	—	Concept Set extent	—	ext
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 instSupConcept lowerPolar Set Set.instInter 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_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 instInfConcept upperPolar Set Set.instInter extent	—	—
intent_injective 📖	mathematical	—	Concept Set intent	—	ext'
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 instSupConcept Set Set.instInter	—	—
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
lowerPolar_intent 📖	mathematical	—	lowerPolar intent extent	—	—
mem_extent_of_rel_extent 📖	—	Set Set.instMembership extent	—	—	lowerPolar_intent trans rel_extent_intent
mem_intent_of_intent_rel 📖	—	Set Set.instMembership intent	—	—	upperPolar_extent trans rel_extent_intent
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
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_extent 📖	mathematical	—	extent Function.swap swap intent	—	—
swap_intent 📖	mathematical	—	intent Function.swap swap extent	—	—
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	—	—

(root)

Definitions

Name	Category	Theorems
Concept 📖	CompData	28 math math: Concept.intent_bot, Concept.extent_sSup, Concept.extent_iInf, Concept.intent_sSup, Concept.intent_iInf, Concept.intent_inf, Concept.intent_subset_intent_iff, Concept.intent_iSup, Concept.swap_le_swap_iff, Concept.extent_injective, Concept.extent_iSup, Concept.swapEquiv_apply, Concept.intent_sup, Concept.intent_ssubset_intent_iff, Concept.extent_subset_extent_iff, Concept.intent_sInf, Concept.extent_sup, Concept.strictAnti_intent, Concept.swap_lt_swap_iff, Concept.intent_top, Concept.extent_top, Concept.extent_inf, Concept.strictMono_extent, Concept.swapEquiv_symm_apply, Concept.extent_ssubset_extent_iff, Concept.extent_bot, Concept.extent_sInf, Concept.intent_injective
lowerPolar 📖	CompOp	18 math math: lowerPolar_swap, lowerPolar_union, Concept.lowerPolar_intent, Concept.extent_sSup, lowerPolar_anti, lowerPolar_iUnion₂, subset_upperPolar_lowerPolar, gc_upperPolar_lowerPolar, lowerPolar_empty, subset_lowerPolar_upperPolar, upperPolar_lowerPolar_upperPolar, Concept.extent_iSup, lowerPolar_iUnion, Concept.extent_sup, lowerPolar_upperPolar_lowerPolar, upperPolar_swap, Concept.extent_bot, subset_upperPolar_iff_subset_lowerPolar
upperPolar 📖	CompOp	18 math math: lowerPolar_swap, subset_upperPolar_lowerPolar, Concept.intent_iInf, Concept.intent_inf, gc_upperPolar_lowerPolar, upperPolar_union, upperPolar_empty, subset_lowerPolar_upperPolar, upperPolar_lowerPolar_upperPolar, Concept.intent_sInf, upperPolar_iUnion₂, Concept.intent_top, lowerPolar_upperPolar_lowerPolar, upperPolar_anti, upperPolar_swap, Concept.upperPolar_extent, subset_upperPolar_iff_subset_lowerPolar, upperPolar_iUnion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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
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_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
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_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