card_le_card_of_leftTotal_unique — Mathlib

English

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

Русский

Если отношение r на конечных множествах α и β правая и слева полной, то |α| ≤ |β|.

LaTeX

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

Lean4

theorem card_le_card_of_leftTotal_unique (h₁ : LeftTotal r) (h₂ : LeftUnique r) : Fintype.card α ≤ Fintype.card β :=
  card_le_card_of_forall_subsingleton r (by simpa using h₁) fun _ _ _ ha₁ _ ha₂ ↦ h₂ ha₁.2 ha₂.2

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