card_Ioo — Mathlib

English

For integers a < b, the open interval Ioo(a,b) contains exactly b−a−1 integers; hence |Ioo(a,b)| = max(0, b−a−1).

Русский

Для целых a < b открытый интервал Ioo(a,b) содержит ровно b−a−1 целых чисел; кардинал равен max(0, b−a−1).

LaTeX

$$$\\lvert \\mathrm{Ioo}(a,b)\\rvert = \\max\\{0,\, b - a - 1\\}$$$

Lean4

@[simp]
theorem card_Ioo : #(Ioo a b) = (b - a - 1).toNat :=
  (card_map _).trans <| card_range _

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