isEmpty_of_card_lt — Mathlib

English

If |β| < |α| there is no injective map α ↪ β.

Русский

Если |β| < |α|, то не существует инъективного отображения α ↪ β.

LaTeX

$$$\\text{There is no injective } f: α \\to β.$$$

Lean4

/-- If `‖β‖ < ‖α‖` there are no embeddings `α ↪ β`.
This is a formulation of the pigeonhole principle.

Note this cannot be an instance as it needs `h`. -/
@[simp]
theorem isEmpty_of_card_lt [Fintype α] [Fintype β] (h : Fintype.card β < Fintype.card α) : IsEmpty (α ↪ β) :=
  ⟨fun f =>
    let ⟨_x, _y, ne, feq⟩ := Fintype.exists_ne_map_eq_of_card_lt f h
    ne <| f.injective feq⟩

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