congr_left — Mathlib

English

If h₁ is a left inverse on s and f maps s into t, and f₁' and f₂' agree on t, then h₂ is a left inverse on s for f₂'.

Русский

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

LaTeX

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

Lean4

theorem congr_left (h₁ : LeftInvOn f₁' f s) {t : Set β} (h₁' : MapsTo f s t) (heq : EqOn f₁' f₂' t) :
    LeftInvOn f₂' f s := fun _ hx => heq (h₁' hx) ▸ h₁ hx

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