card_Ioc — Mathlib

English

The cardinality of Finset.Ioc s t equals the Icc cardinality minus 1: #(Finset.Ioc s t) = card_Icc s t − 1.

Русский

Число элементов Finset.Ioc s t равно кардинальности Icc минус 1.

LaTeX

$$$\\#(\\mathrm{Finset}.Ioc\\ s\\ t) = \\#(\\mathrm{Finset}.Icc\\ s\\ t) - 1$$$

Lean4

theorem card_Ioc : #(Finset.Ioc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 1 := by
  rw [Finset.card_Ioc_eq_card_Icc_sub_one, card_Icc]

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