Theorem upperPolar_lowerPolar_monotone

Modification history

2026-03-21 06:41

Mathlib/Order/Concept.lean

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

Added upperPolar_lowerPolar_monotone View on Github →