Theorem iInf_iSup_of_antitone

Modification history

2026-04-13 06:55
Mathlib/Data/Set/Finite/Lattice.lean
chore(Data/Set/Finite/Lattice): use `to_dual` (#37051)
Deleted iInf_iSup_of_antitoneView on Github →
2026-02-04 14:37
Mathlib/Data/Set/Finite/Lattice.lean
chore(Data/Set/Finite): rename to root namespace (#34790) …
Added iInf_iSup_of_antitoneView on Github →