Commit 2026-02-04 14:37 adc580b2

View on Github →

chore(Data/Set/Finite): rename to root namespace (#34790) These theorems have no connection with Set.

Estimated changes

Modified Mathlib/Data/Set/Finite/Lattice.lean

deleted theorem Set.iInf_iSup_of_antitone

deleted theorem Set.iInf_iSup_of_monotone

deleted theorem Set.iSup_iInf_of_antitone

deleted theorem Set.iSup_iInf_of_monotone

added theorem iInf_iSup_of_antitone

added theorem iInf_iSup_of_monotone

added theorem iSup_iInf_of_antitone

added theorem iSup_iInf_of_monotone