encard_strictMono — Mathlib

English

For finite α, encard is strictly monotone: if S ⊂ T then encard(S) < encard(T).

Русский

Для конечного множества α функция encard строго возрастает: если S ⊂ T, то encard(S) < encard(T).

LaTeX

$$$[\text{Finite } \alpha] \Rightarrow (S \subset T \Rightarrow \operatorname{encard}(S) < \operatorname{encard}(T))$$$

Lean4

theorem encard_strictMono [Finite α] : StrictMono (encard : Set α → ℕ∞) := fun _ _ h ↦ (toFinite _).encard_lt_encard h

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