Commit 2023-01-27 10:13 5f8f4e0d

View on Github →

feat: port Topology.NhdsSet (#1875)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

modified theorem subset_interior_iff_nhds

Created Mathlib/Topology/NhdsSet.lean

added theorem Continuous.tendsto_nhdsSet

added theorem IsOpen.mem_nhdsSet

added theorem bUnion_mem_nhdsSet

added theorem hasBasis_nhdsSet

added theorem mem_nhdsSet_empty

added theorem mem_nhdsSet_iff_exists

added theorem mem_nhdsSet_iff_forall

added theorem mem_nhdsSet_interior

added theorem monotone_nhdsSet

added def nhdsSet

added theorem nhdsSet_diagonal

added theorem nhdsSet_empty

added theorem nhdsSet_eq_principal_iff

added theorem nhdsSet_interior

added theorem nhdsSet_mono

added theorem nhdsSet_singleton

added theorem nhdsSet_union

added theorem nhdsSet_univ

added theorem nhds_le_nhdsSet

added theorem principal_le_nhdsSet

added theorem subset_interior_iff_mem_nhdsSet

added theorem union_mem_nhdsSet