Commit 2024-01-16 14:21 b52b6c43

View on Github →

feat: lemmas about NhdsSet (#9674) From sphere-eversion; I'm just submitting these. Thanks to @urkud for some review suggestions.

Estimated changes

Modified Mathlib/Data/Set/Lattice.lean

added theorem sSup_iUnion

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.Eventually.forall_mem

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem nhdsSet_prod_le

Modified Mathlib/Topology/Constructions.lean

added theorem Filter.Eventually.prod_nhdsSet

added theorem Filter.eventually_nhdsSet_prod_iff

added theorem nhdsSet_prod_le

Modified Mathlib/Topology/NhdsSet.lean

added theorem Filter.Eventually.eventually_nhdsSet

added theorem Filter.Eventually.union

added theorem Filter.Eventually.union_nhdsSet

added theorem IsClosed.nhdsSet_le_sup'

added theorem IsClosed.nhdsSet_le_sup

added theorem eventually_nhdsSet_iUnion

added theorem eventually_nhdsSet_iUnion₂

added theorem nhdsSet_iUnion

added theorem nhdsSet_inter_le