theorem Set.ncard_image2_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (hs : s.Finite) (ht : t.Finite) : (image2 f s t).ncard ≤ s.ncard * t.ncard

theorem Set.Infinite.exists_superset_ncard_eq' {α : Type u_1} {s t : Set α} (ht : t.Infinite) (hst : s ⊆ t) (hs : s.Finite) {k : ℕ} (hsk : s.ncard ≤ k) : ∃ (s' : Set α), s'.Finite ∧ s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k

theorem Set.exists_superset_ncard_eq {α : Type u_1} {s : Set α} {k : ℕ} [Infinite α] (hs : s.Finite) (hsk : s.ncard ≤ k) : ∃ (t : Set α), t.Finite ∧ s ⊆ t ∧ t.ncard = k

theorem Set.exists_subset_ncard_eq {α : Type u_1} {s : Set α} {k : ℕ} (hs : s.Finite) (hks : k ≤ s.ncard) : ∃ t ⊆ s, t.Finite ∧ t.ncard = k

theorem Set.exists_ncard_eq (α : Type u_1) [Infinite α] (k : ℕ) : ∃ (s : Set α), s.Finite ∧ s.ncard = k