set_finite_iff — Mathlib

English

If two sets s and t are in bijection, then s is finite iff t is finite.

Русский

Если множества s и t эквивалентны (существует биекция между ними), то s конечно тогда и только тогда, когда t конечно.

LaTeX

$$$ s \\simeq t \\Rightarrow \\text{Finite}(s) \\iff \\text{Finite}(t) $$$

Lean4

theorem set_finite_iff {s : Set α} {t : Set β} (hst : s ≃ t) : s.Finite ↔ t.Finite := by
  simp_rw [← Set.finite_coe_iff, hst.finite_iff]

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