card_lt_of_injective_not_surjective

English

If f: α → β is injective and not surjective, then card α < card β.

Русский

Если f: α → β инъективна и не сюръективна, то card α < card β.

LaTeX

$$$f:\alpha \to \beta$ injective ∧ ¬Surjective f \Rightarrow |\alpha| < |\beta|$$

Lean4

theorem card_lt_of_injective_not_surjective (f : α → β) (h : Function.Injective f) (h' : ¬Function.Surjective f) :
    card α < card β :=
  let ⟨_y, hy⟩ := not_forall.1 h'
  card_lt_of_injective_of_notMem f h hy

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