Commit 2023-11-03 16:55 721d46e8

View on Github →

feat: characterise independence in compactly-generated lattices (#8154) Also some loosely-related short lemmas

Estimated changes

Modified Mathlib/Order/CompactlyGenerated.lean

added theorem CompleteLattice.independent_iff_supIndep_of_injOn

Modified Mathlib/Order/CompleteLattice.lean

added theorem biInf_congr

added theorem biSup_congr

Modified Mathlib/Order/Disjoint.lean

added theorem disjoint_of_subsingleton

Modified Mathlib/Order/SupIndep.lean

added theorem CompleteLattice.Independent.injOn

added theorem CompleteLattice.Independent.supIndep'