Commit 2023-03-17 12:44 27f3e683

View on Github →

feat: port Topology.Algebra.WithZeroTopology (#2703)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/WithZeroTopology.lean

added theorem WithZeroTopology.Iio_mem_nhds

added theorem WithZeroTopology.Iio_mem_nhds_zero

added theorem WithZeroTopology.hasBasis_nhds_of_ne_zero

added theorem WithZeroTopology.hasBasis_nhds_units

added theorem WithZeroTopology.hasBasis_nhds_zero

added theorem WithZeroTopology.isClosed_iff

added theorem WithZeroTopology.isOpen_Iio

added theorem WithZeroTopology.isOpen_iff

added theorem WithZeroTopology.nhds_coe_units

added theorem WithZeroTopology.nhds_eq_update

added theorem WithZeroTopology.nhds_of_ne_zero

added theorem WithZeroTopology.nhds_zero

added theorem WithZeroTopology.nhds_zero_of_units

added theorem WithZeroTopology.singleton_mem_nhds_of_ne_zero

added theorem WithZeroTopology.singleton_mem_nhds_of_units

added theorem WithZeroTopology.t3Space

added theorem WithZeroTopology.tendsto_of_ne_zero

added theorem WithZeroTopology.tendsto_units

added theorem WithZeroTopology.tendsto_zero

Modified Mathlib/Topology/NhdsSet.lean

added theorem disjoint_nhdsSet_principal

added theorem disjoint_principal_nhdsSet