congr_right — Mathlib

English

If h₁ is a left inverse on s and f₁ and f₂ agree on s, then h₁ is also a left inverse on s for f₂.

Русский

Если h₁ — левый обратный на s и f₁ совпадает с f₂ на s, то h₁ остаётся левым обратным на s для f₂.

LaTeX

$$$$ (h_1 : \\text{LeftInvOn } f_1' f s) \\land (heq : \\text{EqOn } f_1 f_2 s) \\Rightarrow \\text{LeftInvOn } f_1' f_2 s. $$$$

Lean4

theorem congr_right (h₁ : LeftInvOn f₁' f₁ s) (heq : EqOn f₁ f₂ s) : LeftInvOn f₁' f₂ s := fun _ hx => heq hx ▸ h₁ hx

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