Commit 2026-04-08 12:57 d96e9579

View on Github →

feat: express filter as supremum of principal filter and free filter (#31242) Prove a filter is free iff it is smaller than the cofinite filter. Prove that every filter decomposes as the disjoint supremum of a principal filter and a free filter.

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.hnot_principal

added theorem Filter.principal_sdiff_principal

Modified Mathlib/Order/Filter/Cofinite.lean

added theorem boundary_le_cofinite

added theorem boundary_principal

added theorem existsUnique_eq_principal_sup_free

added theorem exists_eq_principal_sup_free

added theorem le_cofinite_iff_boundary

added theorem le_cofinite_iff_ker

Modified Mathlib/Order/Heyting/Boundary.lean

added theorem Coheyting.boundary_boundary

deleted theorem Coheyting.boundary_idem

added theorem Coheyting.sdiff_boundary_self

Modified Mathlib/Order/Lattice.lean

added theorem sup_rotate'

added theorem sup_rotate