finite_iff — Mathlib

English

For a bijection f: α ≃ β, α is finite if and only if β is finite.

Русский

Для биекции f: α ≃ β верно: конечность α эквивалентна конечности β.

LaTeX

$$$\\forall f:\\\\alpha \\\\simeq \\\\beta, \\\\operatorname{Finite}(\\\\alpha) \iff \\\\operatorname{Finite}(\\\\beta).$$$

Lean4

theorem finite_iff (f : α ≃ β) : Finite α ↔ Finite β :=
  ⟨fun _ => Finite.of_equiv _ f, fun _ => Finite.of_equiv _ f.symm⟩

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