countP_pos

Mathlib.Data.Multiset.Count

URI: https://scilib.ai/kg/mathlib#Multiset.countP_pos

English

0 < countP p s if and only if there exists an element a in s with p a.

Русский

0 < countP p s ⇔ существует элемент a в s с p(a).

LaTeX

$$$0 < \operatorname{countP}(p, s) \iff \exists a \in s, p(a)$$$

Lean4

theorem countP_pos {s} : 0 < countP p s ↔ ∃ a ∈ s, p a :=
  Quot.inductionOn s fun _l => by simp

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

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

Разделы

Аффилиация

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