Commit 2025-04-11 01:58 25569eb4
View on Github →chore(Data/ENat): golf exists_eq_iInf (#23931)
This allows us to remove an unnecessary import. Also we move the lemma directly below its corresponding iSup lemma for consistency.
chore(Data/ENat): golf exists_eq_iInf (#23931)
This allows us to remove an unnecessary import. Also we move the lemma directly below its corresponding iSup lemma for consistency.