count_false

Mathlib.Data.Nat.Count

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

English

Equivalently, there exists m < n with p(m) if and only if count(p,n) ≠ 0.

Русский

Существует m < n с p(m) тогда и только тогда, когда count(p,n) ≠ 0.

LaTeX

$$Iff(\operatorname{count}(p,n) \neq 0, \exists m < n,\; p(m))$$

Lean4

@[simp]
theorem count_false (n : ℕ) : count (fun _ ↦ False) n = 0 :=
  count_of_forall_not fun _ _ ↦ id

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

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

Разделы

Аффилиация

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