Principle_of_Counting

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

named-theoremsnatural-numbersproofwiki

Let $T$ be a set such that $T \sim \N_n$ . Then $\forall m \in \N: n \ne m \implies T \nsim \N_m$

Preamble

import Mathlib.Data.Fintype.Card

Formal statement

theorem Principle_of_Counting {T : Type _} [Fintype T] (n : ℕ) (h : Fintype.card T = n) (m : ℕ) (hm : m ≠ n) : ¬ Nonempty (T ≃ Fin m) := by sorry

Source