Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-28 19:16 afefdcbb

View on Github →

chore(topology): move general theorems to the corresponding theories

Estimated changes

Created algebra/default.lean

Modified algebra/field.lean

added theorem inv_le_inv

added theorem one_lt_inv

Modified algebra/ordered_group.lean

added theorem lt_sub_iff

added theorem sub_lt_iff

Modified algebra/ordered_ring.lean

added theorem one_lt_two

Modified algebra/ring.lean

added theorem add_div

added theorem div_eq_mul_inv

added theorem neg_inv

Created data/quot.lean

added theorem forall_quotient_iff

added theorem quot_mk_image_univ_eq

Modified data/set/basic.lean

added theorem set.image_preimage_eq_inter_rng

Created data/set/disjointed.lean

added def pairwise

added theorem set.disjoint_disjointed

added def set.disjointed

added theorem set.disjointed_Union

added theorem set.disjointed_induct

added theorem set.disjointed_of_mono

Modified data/set/lattice.lean

added theorem subtype_val_image

Modified data/set/prod.lean

added theorem set.univ_prod_univ

Created data/subtype.lean

added theorem exists_subtype

added theorem forall_subtype

Modified order/complete_lattice.lean

added theorem lattice.binfi_inf

added theorem lattice.infi_bool_eq

added theorem lattice.supr_bool_eq

Modified order/filter.lean

added theorem filter.at_top_ne_bot

added theorem filter.inf_principal_eq_bot

added theorem filter.map_at_top_eq

added theorem filter.mem_at_top

added theorem filter.mem_at_top_iff

added theorem filter.mem_infi_sets_finset

added theorem filter.tendsto_finset_image_at_top_at_top

Modified topology/borel_space.lean

added theorem measure_theory.borel_eq_generate_from_Iio_of_rat

added theorem measure_theory.borel_eq_generate_from_Ioo_of_rat_of_rat

added theorem measure_theory.is_topological_basis_Ioo_of_rat_of_rat

Modified topology/continuity.lean

added theorem continuous_if

deleted theorem image_preimage_eq_inter_rng

deleted theorem subtype.val_image

deleted theorem univ_prod_univ

Modified topology/ennreal.lean

deleted theorem supr_bool_eq

Modified topology/infinite_sum.lean

deleted theorem add_div

deleted theorem at_top_ne_bot

deleted theorem cauchy_iff

deleted theorem filter.mem_at_top

deleted theorem filter.mem_infi_sets_finset

deleted theorem forall_and_distrib'

deleted theorem map_at_top_eq

deleted theorem mem_at_top_iff

deleted theorem mem_closure_of_tendsto

deleted theorem tendsto_finset_image_at_top_at_top

Modified topology/lebesgue_measure.lean

deleted theorem borel_eq_generate_from_Iio_of_rat

deleted theorem borel_eq_generate_from_Ioo_of_rat_of_rat

deleted theorem inv_le_inv

deleted theorem is_topological_basis_Ioo_of_rat_of_rat

deleted theorem is_topological_basis_of_open_of_nhds

deleted theorem max_of_rat_of_rat

deleted theorem min_of_rat_of_rat

Modified topology/limits.lean

deleted theorem div_eq_mul_inv

deleted theorem exists_lt_of_nat

deleted theorem int_of_nat_eq_of_nat

deleted theorem neg_inv

deleted def of_nat

deleted theorem of_nat_add

deleted theorem of_nat_bit0

deleted theorem of_nat_bit1

deleted theorem of_nat_le_of_nat

deleted theorem of_nat_le_of_nat_iff

deleted theorem of_nat_mul

deleted theorem of_nat_one

deleted theorem of_nat_pos

deleted theorem of_nat_sub

deleted theorem one_lt_inv

deleted theorem rat_coe_eq_of_nat

deleted theorem rat_of_nat_eq_of_nat

deleted theorem real_of_rat_of_nat_eq_of_nat

deleted theorem zero_le_of_nat

Modified topology/measurable_space.lean

deleted def pairwise

deleted theorem set.disjoint_disjointed

deleted def set.disjointed

deleted theorem set.disjointed_Union

deleted theorem set.disjointed_induct

deleted theorem set.disjointed_of_mono

Modified topology/metric_space.lean

deleted theorem exists_subtype

Created topology/of_nat.lean

added theorem exists_lt_of_nat

added theorem int_of_nat_eq_of_nat

added def of_nat

added theorem of_nat_add

added theorem of_nat_bit0

added theorem of_nat_bit1

added theorem of_nat_le_of_nat

added theorem of_nat_le_of_nat_iff

added theorem of_nat_mul

added theorem of_nat_one

added theorem of_nat_pos

added theorem of_nat_sub

added theorem rat_coe_eq_of_nat

added theorem rat_of_nat_eq_of_nat

added theorem real_of_rat_of_nat_eq_of_nat

added theorem zero_le_of_nat

Modified topology/real.lean

deleted theorem forall_subtype_iff

deleted theorem lt_sub_iff

added theorem max_of_rat_of_rat

added theorem min_of_rat_of_rat

deleted theorem one_lt_two

deleted theorem orderable_topology_of_nhds_abs

deleted theorem quot_mk_image_univ_eq

deleted theorem sub_lt_iff

Modified topology/topological_space.lean

added theorem closure_compl

added def frontier

added theorem frontier_eq_closure_inter_closure

added theorem interior_compl

added theorem mem_closure_of_tendsto

added theorem topological_space.is_topological_basis_of_open_of_nhds

Modified topology/topological_structures.lean

deleted theorem binfi_inf

deleted theorem closure_compl

deleted theorem continuous_if

deleted def frontier

deleted theorem frontier_eq_closure_inter_closure

deleted theorem inf_principal_eq_bot

deleted theorem interior_compl

added theorem orderable_topology_of_nhds_abs

Modified topology/uniform_space.lean

added theorem cauchy_iff

deleted theorem forall_quotient_iff