feat(SetTheory/Cardinal): sInf_eq_zero_iff, iInf_eq_zero_iff (#11132

)

Add the two lemmas

```lean
lemma sInf_eq_zero_iff {s : Set Cardinal} : sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0 := by
```

and

```lean
lemma iInf_eq_zero_iff {ι : Sort*} {f : ι → Cardinal} :
    (⨅ i, f i) = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0 := by
```

Feel free to golf.

From AperiodicMonotilesLean.

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -795,6 +795,19 @@ theorem sInf_empty : sInf (∅ : Set Cardinal.{u}) = 0 :=
   dif_neg Set.not_nonempty_empty
 #align cardinal.Inf_empty Cardinal.sInf_empty
 
+lemma sInf_eq_zero_iff {s : Set Cardinal} : sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0 := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rcases s.eq_empty_or_nonempty with rfl | hne
+    · exact Or.inl rfl
+    · exact Or.inr ⟨sInf s, csInf_mem hne, h⟩
+  · rcases h with rfl | ⟨a, ha, rfl⟩
+    · exact Cardinal.sInf_empty
+    · exact eq_bot_iff.2 (csInf_le' ha)
+
+lemma iInf_eq_zero_iff {ι : Sort*} {f : ι → Cardinal} :
+    (⨅ i, f i) = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0 := by
+  simp [iInf, sInf_eq_zero_iff]
+
 /-- Note that the successor of `c` is not the same as `c + 1` except in the case of finite `c`. -/
 instance : SuccOrder Cardinal :=
   SuccOrder.ofSuccLeIff (fun c => sInf { c' | c < c' })