Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 09:50 6d0f40a6

View on Github →

chore(topology/algebra/ordered): use continuous_at, rename (#3231)

  • rename Sup_mem_of_is_closed and Inf_mem_of_is_closed to is_closed.Sup_mem and is_closed.Inf_mem, similarly with cSup and cInf;
  • make Sup_of_continuous etc take continuous_at instead of continuous, rename to Sup_of_continuous_at_of_monotone etc, similarly with cSup/cInf.

Estimated changes

modified theorem Inf_mem_closure
deleted theorem Inf_mem_of_is_closed
deleted theorem Inf_of_continuous'
deleted theorem Inf_of_continuous
modified theorem Sup_mem_closure
deleted theorem Sup_mem_of_is_closed
deleted theorem Sup_of_continuous'
deleted theorem Sup_of_continuous
deleted theorem cInf_mem_of_is_closed
deleted theorem cSup_mem_of_is_closed
deleted theorem infi_of_continuous'
deleted theorem infi_of_continuous
added theorem is_closed.Inf_mem
added theorem is_closed.Sup_mem
added theorem is_closed.cInf_mem
added theorem is_closed.cSup_mem
deleted theorem supr_of_continuous'
deleted theorem supr_of_continuous
added theorem ennreal.infi_mul_left
added theorem ennreal.infi_mul_right
modified def Gromov_Hausdorff.HD