fix(data/list/min_max): correct names of mem_maximum and mem_minimum (#…

…1162)

* fix(data/list/min_max): correct names of mem_maximum and mem_minimum

* Update denumerable.lean

src/data/equiv/denumerable.lean

@@ -168,7 +168,7 @@ if ht : t = [] then ⟨0, le_antisymm (@bot_le s _ _)
   (le_of_not_gt (λ h, list.not_mem_nil ⊥ $
     by rw [← ht, hmt]; exact h))⟩
 else by letI : inhabited s := ⟨⊥⟩;
-  exact have wf : (list.maximum t).1 < x, by simpa [hmt] using list.mem_maximum ht,
+  exact have wf : (list.maximum t).1 < x, by simpa [hmt] using list.maximum_mem ht,
   let ⟨a, ha⟩ := of_nat_surjective_aux (list.maximum t).2 in
   ⟨a + 1, le_antisymm
     (by rw of_nat; exact succ_le_of_lt (by rw ha; exact wf)) $

src/data/list/min_max.lean

@@ -93,10 +93,10 @@ begin
   cases hc, { simp [hc] }, { simp [hc, mem_foldr_min] }
 end
 
-theorem mem_maximum {l : list α} (h : l ≠ []) : maximum l ∈ l :=
+theorem maximum_mem {l : list α} (h : l ≠ []) : maximum l ∈ l :=
 by { dsimp, rw foldl_eq_foldr max_comm max_assoc, apply mem_maximum_aux h }
 
-theorem mem_minimum {l : list α} (h : l ≠ []) : minimum l ∈ l :=
+theorem minimum_mem {l : list α} (h : l ≠ []) : minimum l ∈ l :=
 by { dsimp, rw foldl_eq_foldr min_comm min_assoc, apply mem_minimum_aux h }
 
 theorem le_maximum_aux_of_mem : Π {a : α} {l}, a ∈ l → a ≤ maximum_aux l