Commit 2026-03-21 06:41 e3365e67

View on Github →

feat: concept generated by set of objects/attributes (#30001)

Estimated changes

Modified Mathlib/Order/Concept.lean

added theorem Concept.extent_ofObjects_of_isExtent

added theorem Concept.intent_ofAttributes_of_isIntent

added theorem Concept.le_ofAttributes_iff

added theorem Concept.le_ofObjects_of_extent_subset

added theorem Concept.leftInvOn_extent_ofObjects

added theorem Concept.leftInvOn_ofObjects_intent

added theorem Concept.leftInverse_ofAttributes_extent

added theorem Concept.leftInverse_ofObjects_extent

added def Concept.ofAttributes

added theorem Concept.ofAttributes_intent

added theorem Concept.ofAttributes_le_of_intent_subset

added theorem Concept.ofObject_le_ofAttribute_iff

added def Concept.ofObjects

added theorem Concept.ofObjects_extent

added theorem Concept.ofObjects_le_iff

added theorem Concept.surjective_ofAttributes

added theorem Concept.surjective_ofObjects

added theorem Order.IsExtent.lowerPolar_upperPolar_subset

added theorem Order.IsIntent.upperPolar_lowerPolar_subset

added def extentClosure

added theorem gc_lowerPolar_upperPolar

added def intentClosure

added theorem lowerPolar_upperPolar_monotone

added theorem upperPolar_lowerPolar_monotone

Modified Mathlib/Order/GaloisConnection/Defs.lean

added theorem GaloisConnection.monotone_l_comp_u