English
Let α be a finite type. For any sets s and t of α, if s is contained in t, then the cardinality of s does not exceed the cardinality of t. In particular, the size of a subset is never larger than the size of the ambient set.
Русский
Пусть α конечного типа. Для любых множеств s, t ⊆ α верно: если s ⊆ t, то |s| ≤ |t|. В частности, множество- подмножество не может быть больше по кардиналу, чем верхнее множество.
LaTeX
$$$ \forall \alpha \ (\text{Finite } \alpha) \ (s,t : Set \alpha),\ s \subseteq t \Rightarrow |s| \le |t| $$$
Lean4
theorem ncard_mono [Finite α] : @Monotone (Set α) _ _ _ ncard := fun _ _ ↦ ncard_le_ncard
