Commit 2026-03-13 12:23 3f94ad86

View on Github →

chore(Order/Concept): IsIntent and IsExtent (#29996) We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances. The fields Concept.intent and Concept.extent already existed, and these serve as unbundled versions of them.

Estimated changes

Modified Mathlib/Order/Concept.lean

deleted theorem Concept.extent_bot

deleted theorem Concept.extent_inf

deleted theorem Concept.extent_sInf

deleted theorem Concept.extent_sSup

deleted theorem Concept.extent_sup

deleted theorem Concept.extent_top

deleted theorem Concept.intent_bot

deleted theorem Concept.intent_inf

deleted theorem Concept.intent_sInf

deleted theorem Concept.intent_sSup

deleted theorem Concept.intent_sup

deleted theorem Concept.intent_top

added theorem Concept.isExtent_extent

added theorem Concept.isExtent_iff_exists_concept

added theorem Concept.isIntent_iff_exists_concept

added theorem Concept.isIntent_intent

added def Concept.ofIsExtent

added def Concept.ofIsIntent

added def Order.IsExtent

added def Order.IsIntent

added theorem Order.isExtent_iff

added theorem Order.isExtent_lowerPolar

added theorem Order.isIntent_iff

added theorem Order.isIntent_upperPolar

added theorem mem_lowerPolar_iff

added theorem mem_lowerPolar_singleton

added theorem mem_upperPolar_iff

added theorem mem_upperPolar_singleton