transPrincipal_apply — Mathlib

English

If f : r ≼i s and g : s ≺i t, then (f.transPrincipal g) a = g(f(a)).

Русский

Если f : r ≼i s и g : s ≺i t, то (f.transPrincipal g) a = g(f(a)).

LaTeX

$$$f.transPrincipal\\ g\\ a = g(f\\ a)$$$

Lean4

@[simp]
theorem transPrincipal_apply [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
    f.transPrincipal g a = g (f a) := by
  rw [InitialSeg.transPrincipal]
  obtain f' | f' := f.principalSumRelIso
  · rw [PrincipalSeg.trans_apply, f.eq_principalSeg]
  · rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

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