Theorem Order.IsExtent.lowerPolar_upperPolar_subset

Modification history

2026-03-21 06:41
Mathlib/Order/Concept.lean
feat: concept generated by set of objects/attributes (#30001)
Added Order.IsExtent.lowerPolar_upperPolar_subsetView on Github →