Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 03:30 cbd67cf4

View on Github →

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

Estimated changes