card_Ioo_finset — Mathlib

English

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

Русский

Если s ⊆ t, кардинальность открытого интервала Ioo(s, t) равна 2^(card(t) − card(s)) − 2.

LaTeX

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

Lean4

/-- Cardinality of an `Ioo` of finsets. -/
theorem card_Ioo_finset (h : s ⊆ t) : (Ioo s t).card = 2 ^ (t.card - s.card) - 2 := by
  rw [card_Ioo_eq_card_Icc_sub_two, card_Icc_finset h]

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