rel_replicate_right — Mathlib

English

Let m be a multiset, a an element, r a binary relation on α, and n ∈ ℕ. Then m Rel r (replicate n a) holds exactly when card m = n and every element x ∈ m satisfies r(x,a).

Русский

Пусть m — мультисет, a — элемент, r — бинарное отношение на α, и n ∈ ℕ. Тогда m Rel r (replicate n a) эквивалентно тому, что card m = n и для каждого x ∈ m выполняется r(x,a).

LaTeX

$$$$ m \\,\\operatorname{Rel}_{r} (\\operatorname{replicate} n a) \\iff \\operatorname{card}(m) = n \\wedge \\forall x \\in m,\\ r(x,a). $$$$

Lean4

theorem rel_replicate_right {m : Multiset α} {a : α} {r : α → α → Prop} {n : ℕ} :
    m.Rel r (replicate n a) ↔ card m = n ∧ ∀ x, x ∈ m → r x a :=
  rel_flip.trans rel_replicate_left

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