cast_ncard_sdiff — Mathlib

English

If s ⊆ t and t is finite, then |t \ s| = |t| − |s| (as elements of an additive group with one, after casting).

Русский

Если s ⊆ t и t конечно, то |t \ s| = |t| − |s| (после приведения к нужному кольцу кардинальности).

LaTeX

$$$$ ((t \ s).ncard : R) = t.ncard - s.ncard $$$$

Lean4

theorem cast_ncard_sdiff {R : Type*} [AddGroupWithOne R] (hst : s ⊆ t) (ht : t.Finite) :
    ((t \ s).ncard : R) = t.ncard - s.ncard := by
  rw [ncard_diff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]

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