card_le_card_of_injective — Mathlib

English

If there exists an injection f: s → t, then |s| ≤ |t|.

Русский

Если существует инъекция f: s → t, то |s| ≤ |t|.

LaTeX

$$There exists an injective function f: s → t ⇒ |s| ≤ |t|$$

Lean4

theorem card_le_card_of_injective {f : s → t} (hf : f.Injective) : #s ≤ #t :=
  by
  rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩
  · simp
  ·
    classical
    let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)
    apply card_le_card_of_injOn f'
    · aesop (add safe unfold Set.MapsTo)
    · intro a₁ ha₁ a₂ ha₂ haa
      rw [mem_coe] at ha₁ ha₂
      simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
      exact Subtype.ext_iff.mp (hf haa)

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