le_min_of_mem

Stream: general

[Kenny Lau]

theorem le_min_of_mem {s : finset α} {a b : α} (h₁ : b ∈ s) (h₂ : a ∈ s.min) : a ≤ b :=
by rcases @inf_le (with_top α) _ _ _ _ _ _ _ h₁ _ rfl with ⟨b', hb, ab⟩;
   cases h₂.symm.trans hb; assumption

[Kenny Lau]

looks like min_le_of_mem to me

[Chris Hughes]

PR it.

[Chris Hughes]

my guess is someone copied the name le_max_of_mem and didn't notice the word order needed changing