pseudoEqual_refl — Mathlib

English

For any object P, the relation of pseudoequality on Over P is reflexive: every pseudoelement is pseudoequal to itself.

Русский

Для произвольного объекта P отношение псевдоэквивалентности на Over P рефлексивно: каждый псевдоэлемент равен самому себе.

LaTeX

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

Lean4

theorem pseudoEqual_refl {P : C} : Reflexive (PseudoEqual P) := fun f =>
  ⟨f.1, 𝟙 f.1, 𝟙 f.1, inferInstance, inferInstance, by simp⟩

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