counting arguments for relations on finsets

Stream: Is there code for X?

[Jakob von Raumer]

Do we have something similar to this?

lemma _root_.right_unique_of_left_total_of_left_unique {α β : Type*} (A : Finset α) (B : Finset β)
    (hcard : #A = #B)
    (R : α → β → Prop)
    (htotal : ∀ a ∈ A, ∃ b ∈ B, R a b)
    (hunique : ∀ a₁ ∈ A, ∀ a₂ ∈ A, ∀ b ∈ B, R a₁ b → R a₂ b → a₁ = a₂) :
    ∀ a ∈ A, ∀ b₁ ∈ B, ∀ b₂ ∈ B, R a b₁ → R a b₂ → b₁ = b₂ :=
  sorry

[Yaël Dillies]

That's very similar to what's in file#Combinatorics/Enumerative/DoubleCounting

[Jakob von Raumer]

Seems like it's the reverse direction to card_le_card_of_forall_subsingleton

[Yaël Dillies]

If it's not in that file, then it's not there! PR welcome :slight_smile: