[STATEMENT]
lemma min_product_empty_singleton[simp]:
  "A \<otimes>\<^sub>m {{||}} = min_set A"
  "{{||}} \<otimes>\<^sub>m A = min_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<otimes>\<^sub>m {{||}} = min_set A &&& {{||}} \<otimes>\<^sub>m A = min_set A
[PROOF STEP]
by (simp_all add: min_product_def)