natCard_mul_le — Mathlib

English

The natural cardinality of the inverse set equals the natural cardinality of the original set: Nat.card(s⁻¹) = Nat.card(s).

Русский

Естественная кардинальность множества обратного образа равна кардинальности исходного множества: Nat.card(s⁻¹) = Nat.card(s).

LaTeX

$$$$ \\mathrm{Nat.card}(s^{-1}) = \\mathrm{Nat.card}(s) $$$$

Lean4

@[to_additive]
theorem natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t :=
  by
  obtain h | h := (s * t).infinite_or_finite
  · simp [Set.Infinite.card_eq_zero h]
  simp only [Nat.card, ← Cardinal.toNat_mul]
  refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_
  aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])

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