card_lt_card — Mathlib

English

If t is finite and s is a proper subset of t, then Nat.card s < Nat.card t.

Русский

Если t конечно, а s ⊊ t, то Nat.card s < Nat.card t.

LaTeX

$$$t.Finite \rightarrow s \subset t \rightarrow Nat.card(s) < Nat.card(t)$$$

Lean4

theorem card_lt_card (ht : t.Finite) (hsub : s ⊂ t) : Nat.card s < Nat.card t :=
  by
  have : Fintype t := Finite.fintype ht
  have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))
  simp only [Nat.card_eq_fintype_card]
  exact Set.card_lt_card hsub

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