count_true

Mathlib.Data.Nat.Count

URI: https://scilib.ai/kg/mathlib#Nat.count_true

English

The count of a predicate that is always true up to n equals n.

Русский

Число истинности предиката, который всегда истинный, до n равно n.

LaTeX

$$$\operatorname{count}(\lambda k. \text{True}, n) = n$$$

Lean4

@[simp]
theorem count_true (n : ℕ) : count (fun _ ↦ True) n = n :=
  count_of_forall fun _ _ ↦ trivial

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

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

Разделы

Аффилиация

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