Theorem IsRelLowerSet.mem_of_le

Modification history

2026-03-10 23:22
Mathlib/Order/UpperLower/Relative.lean
feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions (#33364) …
Added IsRelLowerSet.mem_of_leView on Github →