card_le_card_of_injOn — Mathlib

English

If f maps s into t and f is injective on s, then the cardinality of s is at most the cardinality of t.

Русский

Если f отображает s в t и отображение на s инъективно, то |s| ≤ |t|.

LaTeX

$$MapsTo(f, s, t) ∧ InjOn(f, s) ⇒ |s| ≤ |t|$$

Lean4

theorem card_le_card_of_injOn (f : α → β) (hf : Set.MapsTo f s t) (f_inj : (s : Set α).InjOn f) : #s ≤ #t := by
  classical
    calc
    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

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