entourageProd — Mathlib

English

In a symmetric-relations context, entourageProd preserves symmetry.

Русский

В контексте симметричных отношений entourageProd сохраняет симметрию.

LaTeX

$$IsSymmetricRel(entourageProd u v) given IsSymmetricRel u and IsSymmetricRel v$$

Lean4

theorem entourageProd {u : Set (α × α)} {v : Set (β × β)} (hu : IsSymmetricRel u) (hv : IsSymmetricRel v) :
    IsSymmetricRel (entourageProd u v) :=
  Set.ext fun _ ↦ and_congr hu.mk_mem_comm hv.mk_mem_comm

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