card_Icc_finset — Mathlib

English

If s ⊆ t, the cardinality of the closed interval Icc(s, t) is 2^(t.card − s.card).

Русский

Если s ⊆ t, число элементов в замкнутом интервале Icc(s, t) равно 2^(card(t) − card(s)).

LaTeX

$$\\ (Icc(s,t)).card = 2^{t.card - s.card} $$

Lean4

/-- Cardinality of a non-empty `Icc` of finsets. -/
theorem card_Icc_finset (h : s ⊆ t) : (Icc s t).card = 2 ^ (t.card - s.card) :=
  by
  unfold Finset.Icc instLocallyFiniteOrder LocallyFiniteOrder.ofIcc
  simp [h, card_sdiff_of_subset]

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