Commit 2024-10-15 12:11 f87f0ec9

View on Github →

feat: lemmas about exterior (#17765)

Estimated changes

Modified Mathlib/Order/Filter/Ker.lean

modified theorem Filter.ker_iInf

modified theorem Filter.ker_sInf

Modified Mathlib/Topology/Exterior.lean

added theorem exterior_iInter_subset

modified theorem exterior_iUnion

added theorem exterior_inter_subset

added theorem exterior_sInter_subset

Modified Mathlib/Topology/NhdsSet.lean

added theorem nhdsSet_iInter_le

added theorem nhdsSet_sInter_le