Theorem iInf_iSup_of_monotone

Modification history

2026-02-04 14:37
Mathlib/Data/Set/Finite/Lattice.lean
chore(Data/Set/Finite): rename to root namespace (#34790) …
Added iInf_iSup_of_monotoneView on Github →