Commit 2025-08-27 16:48 34c878ca

View on Github →

feat(Order/Concept): sets in a concept are codisjoint (#26968) ...and other small lemmata.

Estimated changes

Modified Mathlib/Order/Concept.lean

added theorem Concept.codisjoint_extent_intent

added theorem Concept.disjoint_extent_intent

added theorem Concept.mem_extent_of_rel_extent

added theorem Concept.mem_intent_of_intent_rel

added theorem Concept.rel_extent_intent