Embedding relation for finsets/sets

Stream: Is there code for X?

[Daniel Weber]

Are the following definitions anywhere in Mathlib?

def Finset.embeddingRel {α β : Type*} (r : α → β → Prop) (a : Finset α) (b : Finset β) : Prop :=
  ∃ f : a ↪ b, ∀ x : a, r x (f x)

def Set.embeddingRel {α β : Type*} (r : α → β → Prop) (a : Set α) (b : Set β) : Prop :=
  ∃ f : a ↪ b, ∀ x : a, r x (f x)

if not, what would be a good place to add them? These are Finset/Set equivalents of List.SublistForall₂.

[Daniel Weber]

Any suggestions?

[Daniel Weber]

They can be combined to

def embeddingRel {α β : Type*} (r : α → β → Prop) : Prop :=
  ∃ f : α ↪ β, ∀ x, r x (f x)

but embeddingRel isn't a good name, it can be confused with docs#RelEmbedding

[Daniel Weber]

Perhaps this can be ExistsMatching? I see that docs#Fintype.all_card_le_filter_rel_iff_exists_injective uses ∃ f : α → β, Function.Injective f ∧ ∀ x, r x (f x), is that spelling preferred to ∃ f : α ↪ β, ∀ x, r x (f x)?