Commit 2024-01-12 06:00 2a498095

View on Github →

chore(Topology/NhdsSet): rename type variables (#9673) Now we use letters X and Y for topological spaces, not Greek letters.

Estimated changes

Modified Mathlib/Topology/NhdsSet.lean

modified theorem Continuous.tendsto_nhdsSet

modified theorem Continuous.tendsto_nhdsSet_nhds

modified theorem Filter.Eventually.self_of_nhdsSet

modified theorem bUnion_mem_nhdsSet

modified theorem eventually_nhdsSet_iff_exists

modified theorem eventually_nhdsSet_iff_forall

modified theorem hasBasis_nhdsSet

modified theorem mem_nhdsSet_empty

modified theorem mem_nhdsSet_iff_exists

modified theorem mem_nhdsSet_iff_forall

modified theorem monotone_nhdsSet

modified def nhdsSet

modified theorem nhdsSet_diagonal

modified theorem nhdsSet_empty

modified theorem nhdsSet_insert

modified theorem nhdsSet_le

modified theorem nhdsSet_union

modified theorem nhdsSet_univ