Mcongr — Mathlib

English

Mcongr x y holds if there exists a relation r that is a Precongr and relates x and y.

Русский

Mcongr x y истинно тогда, когда существует отношение r, являющееся предконгруэнцией, и связывающее x и y.

LaTeX

$$$$ \\mathrm{Mcongr}\\; x\\; y := \\exists r, \\mathrm{IsPrecongr}\\ r \\land r\\ x\\ y. $$$$

Lean4

/-- Equivalence relation on M-types representing a value of type `Cofix F` -/
def Mcongr {α : TypeVec n} (x y : q.P.M α) : Prop :=
  ∃ r, IsPrecongr r ∧ r x y

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