Commit 2024-11-25 10:13 725d2ded

View on Github →

chore: rename CompleteLattice.Independent/.SetIndependent to iSupIndep/sSupIndep (#19409) These names are shorter, closer to SupIndep and clearer without their namespace.

Estimated changes

added theorem sSupIndep_iff_finite
added theorem iSupIndep.comp'
added theorem iSupIndep.comp
added theorem iSupIndep.injOn
added theorem iSupIndep.injective
added theorem iSupIndep.map_orderIso
added theorem iSupIndep.mono
added theorem iSupIndep.supIndep'
added def iSupIndep
added theorem iSupIndep_def''
added theorem iSupIndep_def'
added theorem iSupIndep_def
added theorem iSupIndep_empty
added theorem iSupIndep_iff_supIndep
added theorem iSupIndep_ne_bot
added theorem iSupIndep_pair
added theorem iSupIndep_pempty
added theorem sSupIndep.mono
added def sSupIndep
added theorem sSupIndep_empty
added theorem sSupIndep_iff
added theorem sSupIndep_pair
added theorem sSupIndep_singleton