Theorem Coheyting.boundary_idem

Modification history

2026-04-08 12:57
Mathlib/Order/Heyting/Boundary.lean
feat: express filter as supremum of principal filter and free filter (#31242) …
Deleted Coheyting.boundary_idemView on Github →
2022-12-06 02:39
Mathlib/Order/Heyting/Boundary.lean
feat: port Order.Heyting.Boundary (#844) …
Added Coheyting.boundary_idemView on Github →