card_le_card_of_rightTotal_unique

English

If a finite relation r on finite types α, β is right-total and right-unique, then |β| ≤ |α|.

Русский

Если отношение r на конечных множествах α и β правосторонне полностью и уникально, тогда |β| ≤ |α|.

LaTeX

$$$$ |\beta| \le |\alpha| $$$$

Lean4

theorem card_le_card_of_rightTotal_unique (h₁ : RightTotal r) (h₂ : RightUnique r) : Fintype.card β ≤ Fintype.card α :=
  card_le_card_of_forall_subsingleton' r (by simpa using h₁) fun _ _ _ ha₁ _ ha₂ ↦ h₂ ha₁.2 ha₂.2

Похожие утверждения