Maximal elements of subsets

Let S : Set J and m : S. If m is not a maximal element of S, then ↑m : J is not maximal in J.

theorem Set.not_isMax_coe {J : Type u} [Preorder J] {S : Set J} (m : ↑S) (hm : ¬IsMax m) : ¬IsMax ↑m

theorem Set.not_isMin_coe {J : Type u} [Preorder J] {S : Set J} (m : ↑S) (hm : ¬IsMin m) : ¬IsMin ↑m