congr_right — Mathlib

English

If h₁ : RightInvOn f' f t, MapsTo f' t s, and heq : EqOn f₁ f₂ s, then RightInvOn f' f₂ t.

Русский

Если h₁ — правый обратный и f' отображает t в s, а f₁ совпадает с f₂ на s, тогда RightInvOn f' f₂ t.

LaTeX

$$$$ \\text{RightInvOn } f' f t \\rightarrow \\text{MapsTo } f' t s \\rightarrow \\text{EqOn } f_1 f_2 s \\rightarrow \\text{RightInvOn } f' f_2 t. $$$$

Lean4

theorem congr_right (h₁ : RightInvOn f' f₁ t) (hg : MapsTo f' t s) (heq : EqOn f₁ f₂ s) : RightInvOn f' f₂ t :=
  LeftInvOn.congr_left h₁ hg heq

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