mathlib

cbd67cf4 - feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971)

feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971) Defines `complete_lattice.independent` Shows that this notion of independence is finitary in compactly generated lattices Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>