card_lt_card — Mathlib

English

If s ⊂ t are finite sets, then the cardinality of s is strictly less than that of t.

Русский

Если s ⊂ t — конечные множества, то мощность s строго меньше мощности t.

LaTeX

$$$ s \\subset t \\Rightarrow |s| < |t| $$$

Lean4

theorem card_lt_card {s t : Set α} [Fintype s] [Fintype t] (h : s ⊂ t) : Fintype.card s < Fintype.card t :=
  Fintype.card_lt_of_injective_not_surjective (Set.inclusion h.1) (Set.inclusion_injective h.1) fun hst =>
    (ssubset_iff_subset_ne.1 h).2 (eq_of_inclusion_surjective hst)

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