card_Ico — Mathlib

English

For integers a ≤ b, the half-open interval Ico(a,b) contains exactly b−a integers; hence |Ico(a,b)| = max(0, b−a).

Русский

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

LaTeX

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

Lean4

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

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