Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 07:18 bb05277f

View on Github →

refactor(topology/algebra/with_zero_topology): review API, golf (#16359)

use γ ≠ 0 instead of units;
deduplicate, golf

Estimated changes

Modified src/algebra/order/with_zero.lean

Modified src/topology/algebra/valued_field.lean

Modified src/topology/algebra/with_zero_topology.lean

added theorem linear_ordered_comm_group_with_zero.Iio_mem_nhds

added theorem linear_ordered_comm_group_with_zero.Iio_mem_nhds_zero

deleted theorem linear_ordered_comm_group_with_zero.directed_lt

modified theorem linear_ordered_comm_group_with_zero.has_basis_nhds_zero

added theorem linear_ordered_comm_group_with_zero.is_closed_iff

added theorem linear_ordered_comm_group_with_zero.is_open_Iio

added theorem linear_ordered_comm_group_with_zero.is_open_iff

modified theorem linear_ordered_comm_group_with_zero.nhds_coe_units

added theorem linear_ordered_comm_group_with_zero.nhds_eq_update

deleted def linear_ordered_comm_group_with_zero.nhds_fun

deleted theorem linear_ordered_comm_group_with_zero.nhds_fun_ok

modified theorem linear_ordered_comm_group_with_zero.nhds_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.nhds_zero

deleted theorem linear_ordered_comm_group_with_zero.nhds_zero_of_ne_zero

modified theorem linear_ordered_comm_group_with_zero.nhds_zero_of_units

deleted theorem linear_ordered_comm_group_with_zero.pure_le_nhds_fun

modified theorem linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_ne_zero

added theorem linear_ordered_comm_group_with_zero.singleton_mem_nhds_of_units

deleted theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_ne_zero

deleted theorem linear_ordered_comm_group_with_zero.singleton_nhds_of_units

modified theorem linear_ordered_comm_group_with_zero.tendsto_of_ne_zero

modified theorem linear_ordered_comm_group_with_zero.tendsto_units

modified theorem linear_ordered_comm_group_with_zero.tendsto_zero

Modified src/topology/order.lean

added theorem topological_space.nhds_mk_of_nhds_single

Modified src/topology/separation.lean

added theorem t3_space.of_lift'_closure