Cardinality_of_Subset_of_Finite_Set

Proved

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

cardinalityproofwikiset-theorysubsets

Let $A$ and $B$ be finite sets such that $A \subseteq B$ . Let $\card B = n$ where $\card {\, \cdot \,}$ denotes cardinality. Then $\card A \le n$ .

Preamble

import Mathlib.Data.Finset.Card

Formal statement

theorem Cardinality_of_Subset_of_Finite_Set {S : Type _} [Fintype S] (A B : Finset S) (h : A ⊆ B) : A.card ≤ B.card := by sorry

Source