pseudoEqual_symm — Mathlib

English

For Over P, the pseudoequality relation is symmetric: if a is pseudoequal to b, then b is pseudoequal to a.

Русский

Для Over P отношение псевдоэквивалентности симметрично: если a псевдоэквивалентно b, то b псевдоэквивалентно a.

LaTeX

$$$\\forall a,b,\\; \\mathrm{PseudoEqual}(P)(a,b) \\Rightarrow \\mathrm{PseudoEqual}(P)(b,a)$$$

Lean4

theorem pseudoEqual_symm {P : C} : Symmetric (PseudoEqual P) := fun _ _ ⟨R, p, q, ep, Eq, comm⟩ =>
  ⟨R, q, p, Eq, ep, comm.symm⟩

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