Commit 2026-09-28 21:29 bc5fddb8
View on Github →chore(Order/Filter/Germ): move lemmas (#44302) These lemmas don't really have anything to do with germs or dependent products on filters, so they are moved to an earlier file.
chore(Order/Filter/Germ): move lemmas (#44302) These lemmas don't really have anything to do with germs or dependent products on filters, so they are moved to an earlier file.