bijective_iff_surjective_and_card

English

For f: α → β, Bijective f is equivalent to Surjective f and card α = card β.

Русский

Для отображения f: α → β биективность эквивалентна сюръективности и равенству кардиналов α и β.

LaTeX

$$$\\text{Bijective } f \\iff (\\text{Surjective } f \\land \\operatorname{card} \\alpha = \\operatorname{card} \\beta)$$$

Lean4

theorem bijective_iff_surjective_and_card (f : α → β) : Bijective f ↔ Surjective f ∧ card α = card β :=
  ⟨fun h => ⟨h.2, card_of_bijective h⟩, fun h => ⟨h.1.injective_of_fintype <| equivOfCardEq h.2, h.1⟩⟩

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