eq_relIso — Mathlib

English

For IsWellOrder β s and InitialSeg f, g : InitialSeg r s, the equality of their RelIso coe components implies equality of f and g.

Русский

Для IsWellOrder β s и InitialSeg f, g: InitialSeg r s, равенство коe-компонент RelIso влечёт равенство f и g.

LaTeX

$$$[IsWellOrder \\ β \\ s] (f : r ≼i s) (g : r \\equiv_r s) (a) : (RelIso.instFunLike.coe g a) = (InitialSeg.instFunLike.coe f a).$$$

Lean4

theorem eq_relIso [IsWellOrder β s] (f : r ≼i s) (g : r ≃r s) (a : α) : g a = f a :=
  InitialSeg.eq g.toInitialSeg f a

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