finite_iff_exists_equiv_fin — Mathlib

English

If α is finite and s ⊆ α, then card(α) ≤ card(s) implies s = univ.

Русский

Если α конечна и s ⊆ α, то card(α) ≤ card(s) влечёт, что s = α.

LaTeX

$$$[\\Finite(\\alpha)] \\Rightarrow \\forall s \\subseteq \\alpha, \\operatorname{card}(\\alpha) \\le \\operatorname{card}(s) \\Rightarrow s = \mathrm{univ}.$$$

Lean4

theorem finite_iff_exists_equiv_fin {α : Sort*} : Finite α ↔ ∃ n, Nonempty (α ≃ Fin n) :=
  ⟨fun ⟨e⟩ => ⟨_, ⟨e⟩⟩, fun ⟨_, ⟨e⟩⟩ => ⟨e⟩⟩

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