Theorem CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent

Modification history

2024-11-25 10:13

Mathlib/Order/CompactlyGenerated/Basic.lean

chore: rename `CompleteLattice.Independent`/`.SetIndependent` to `iSupIndep`/`sSupIndep` (#19409) …

Deleted CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent View on Github →

2024-10-09 07:18

Mathlib/Order/CompactlyGenerated/Basic.lean

feat: in a WellFoundedLT CompleteLattice, Independent sets are finite (#17525) …

Added CompleteLattice.WellFoundedGT.finite_ne_bot_of_independent View on Github →