theorem
List.Sublist.le_countP :
∀ {α : Type u_1} {l₁ l₂ : List α},
l₁.Sublist l₂ → ∀ (p : α → Bool), List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
The number of elements satisfying a predicate in a sublist is at least the number of elements satisfying the predicate in the list, minus the difference in the lengths.
theorem
List.IsPrefix.le_countP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
l₁ <+: l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
theorem
List.IsSuffix.le_countP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
l₁ <:+ l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
theorem
List.IsInfix.le_countP :
∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
l₁ <:+: l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
theorem
List.le_countP_tail :
∀ {α : Type u_1} {p : α → Bool} (l : List α), List.countP p l - 1 ≤ List.countP p l.tail
The number of elements satisfying a predicate in the tail of a list is at least one less than the number of elements satisfying the predicate in the list.
theorem
List.Sublist.le_count
{α : Type u_1}
[BEq α]
{l₁ : List α}
{l₂ : List α}
(s : l₁.Sublist l₂)
(a : α)
:
List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
theorem
List.IsPrefix.le_count
{α : Type u_1}
[BEq α]
{l₁ : List α}
{l₂ : List α}
(s : l₁ <+: l₂)
(a : α)
:
List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
theorem
List.IsSuffix.le_count
{α : Type u_1}
[BEq α]
{l₁ : List α}
{l₂ : List α}
(s : l₁ <:+ l₂)
(a : α)
:
List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
theorem
List.IsInfix.le_count
{α : Type u_1}
[BEq α]
{l₁ : List α}
{l₂ : List α}
(s : l₁ <:+: l₂)
(a : α)
:
List.count a l₂ - (l₂.length - l₁.length) ≤ List.count a l₁
theorem
List.le_count_tail
{α : Type u_1}
[BEq α]
(a : α)
(l : List α)
:
List.count a l - 1 ≤ List.count a l.tail