eqOn_of_leftInvOn_of_rightInvOn — Mathlib

English

If f1' and f' agree on t via left inverse and f2' and f agree on t via right inverse, and f2' maps t to s, then f1' and f2' are equal on t.

Русский

Если f1' и f согласованы через левую обратную на t, а f2' и f через правую на t, и f2' отображает t в s, то на t выполняется равенство f1' = f2'.

LaTeX

$$$$\\operatorname{LeftInvOn}(f_1', f, s) \\land \\operatorname{RightInvOn}(f_2', f, t) \\land \\operatorname{MapsTo}(f_2', t, s) \\Rightarrow \\operatorname{EqOn}(f_1', f_2', t).$$$$

Lean4

theorem eqOn_of_leftInvOn_of_rightInvOn (h₁ : LeftInvOn f₁' f s) (h₂ : RightInvOn f₂' f t) (h : MapsTo f₂' t s) :
    EqOn f₁' f₂' t := fun y hy =>
  calc
    f₁' y = (f₁' ∘ f ∘ f₂') y := congr_arg f₁' (h₂ hy).symm
    _ = f₂' y := h₁ (h hy)

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