card_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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