rel — Mathlib

English

There is a straightforward translation functor that converts a PreEnvelGroupRel' relation into the corresponding PreEnvelGroupRel relation.

Русский

Существует тривиальный переходник, переводящий отношение PreEnvelGroupRel' в соответствующее PreEnvelGroupRel.

LaTeX

$$$\forall R, a,b:\ PreEnvelGroupRel'\!\_R\ a\ b \Rightarrow PreEnvelGroupRel\_R\ a\ b.$$$

Lean4

/-- A quick way to convert a `PreEnvelGroupRel'` to a `PreEnvelGroupRel`.
-/
theorem rel {R : Type u} [Rack R] {a b : PreEnvelGroup R} : PreEnvelGroupRel' R a b → PreEnvelGroupRel R a b :=
  PreEnvelGroupRel.rel

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