rel_refl_of_refl_on — Mathlib

English

If a relation r is reflexive on every element of a multiset m (i.e., r x x for all x ∈ m), then Rel r m m holds.

Русский

Если отношение r является рефлексивным на каждом элементе мультисета m (то есть r x x для всех x ∈ m), то Rel r m m верно.

LaTeX

$$$\bigl(\forall x \in m,\ r\ x\ x\bigr) \rightarrow Rel\ r\ m\ m$$$

Lean4

theorem rel_refl_of_refl_on {m : Multiset α} {r : α → α → Prop} : (∀ x ∈ m, r x x) → Rel r m m :=
  by
  refine m.induction_on ?_ ?_
  · intros
    apply Rel.zero
  · intro a m ih h
    exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

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