Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 22:59 e93996cf

View on Github →

feat(topology/instances/discrete): instances for the discrete topology (#11349) Prove first_countable_topology, second_countable_topology and order_topology for the discrete topology under appropriate conditions like encodable, or being a linear order with pred and succ. These instances give in particular second_countable_topology ℕ and order_topology ℕ

Estimated changes

Modified src/order/filter/bases.lean

added theorem filter.is_countably_generated_pure

Modified src/order/succ_pred/basic.lean

added theorem pred_order.Ici_eq_Ioi_pred'

added theorem pred_order.Ici_eq_Ioi_pred

added theorem pred_order.Iio_eq_Iic_pred'

added theorem pred_order.Iio_eq_Iic_pred

added theorem pred_order.le_pred_iff_of_not_is_min

added theorem pred_order.pred_lt_iff_of_not_is_min

added theorem pred_order.pred_lt_of_not_is_min

added theorem succ_order.Iic_eq_Iio_succ'

added theorem succ_order.Iic_eq_Iio_succ

added theorem succ_order.Ioi_eq_Ici_succ'

added theorem succ_order.Ioi_eq_Ici_succ

added theorem succ_order.lt_succ_iff_of_not_is_max

added theorem succ_order.lt_succ_of_not_is_max

added theorem succ_order.succ_le_iff_of_not_is_max

Modified src/topology/bases.lean

Created src/topology/instances/discrete.lean

Modified src/topology/order.lean

added theorem topological_space.is_open_generate_from_of_mem