card_Ici

Mathlib.Order.Interval.Finset.Fin

URI: https://scilib.ai/kg/mathlib#Fin.card_Ici

English

For any a ∈ Fin n, the number of elements in the closed interval [a, ∞) ∩ Fin n equals n − a.

Русский

Для любого a ∈ Fin n число элементов в интервале [a, ∞) ∩ Fin n равно n − a.

LaTeX

$$|Ici(a)| = n − a$$

Lean4

@[simp]
theorem card_Ici : #(Ici a) = n - a := by rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru