forall_coe — Mathlib

English

A property p holds for all elements of the multiset m if and only if p holds for all representatives a with indices i = Fin (count a in m).

Русский

Свойство p выполняется для всех элементов m тогда и только тогда, когда p выполняется для всех представлений a с индексами i = Fin(кол-во a в m).

LaTeX

$$∀ p : m → Prop, (∀ x : m, p x) ↔ ∀ (x : α) (i : Fin (m.count x)), p ⟨x, i⟩$$

Lean4

@[simp]
protected theorem forall_coe (p : m → Prop) : (∀ x : m, p x) ↔ ∀ (x : α) (i : Fin (m.count x)), p ⟨x, i⟩ :=
  Sigma.forall

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