finite_iff_finite — Mathlib

English

If a bijection f sets a bijection between s and t, then s finite iff t finite.

Русский

Если f задаёт биекция между s и t, то s конечно тогда и только тогда, когда t конечно.

LaTeX

$$$\mathrm{BijOn}(f,s,t) \Rightarrow (\mathrm{Finite}(s) \Leftrightarrow \mathrm{Finite}(t))$$$

Lean4

theorem finite_iff_finite {f : α → β} {s : Set α} {t : Set β} (h : BijOn f s t) : s.Finite ↔ t.Finite :=
  ⟨fun h1 ↦ h1.of_surjOn _ h.2.2, fun h1 ↦ h1.of_injOn h.1 h.2.1⟩

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