rel_join — Mathlib

English

If r is a relation on α and s, t are multisets of multisets with h lifting Rel r between s and t (i.e., Rel (Rel r) s t), then s.join and t.join are related by Rel r.

Русский

Пусть r — отношение на α, а s, t — мультимножества над α, причём существует отношение Rel (Rel r) между s и t. Тогда s.join и t.join связаны отношением Rel r.

LaTeX

$$$Rel\\ r\\ s.join\\ t.join$$$

Lean4

theorem rel_join {r : α → β → Prop} {s t} (h : Rel (Rel r) s t) : Rel r s.join t.join := by
  induction h with
  | zero => simp
  | cons hab hst ih => simpa using hab.add ih

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