card_lt_of_injective_of_notMem — Mathlib

English

Let f: α → β be injective and choose b ∈ β not in the image of f. Then card α < card β.

Русский

Пусть f: α → β инъективна и выберем b ∈ β, не принадлежащий изображению f. Тогда card α < card β.

LaTeX

$$$f:\alpha \to \beta$ injective \wedge b\notin \operatorname{Im}(f) \Rightarrow |\alpha| < |\beta|$$

Lean4

theorem card_lt_of_injective_of_notMem (f : α → β) (h : Function.Injective f) {b : β} (w : b ∉ Set.range f) :
    card α < card β :=
  calc
    card α = (univ.map ⟨f, h⟩).card := (card_map _).symm
    _ < card β := Finset.card_lt_univ_of_notMem (x := b) <| by rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

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