mono — Mathlib

English

If f' is a right inverse of f on t and t1 is a subset of t, then f' is a right inverse of f on t1 as well.

Русский

Если f' является правой обратной к f на t, и t1 ⊆ t, тогда f' является правой обратной к f на t1.

LaTeX

$$$$\\operatorname{RightInvOn}(f', f, t) \\\\land t_1 \\subseteq t \;\\Rightarrow \\; \\operatorname{RightInvOn}(f', f, t_1).$$$$

Lean4

theorem mono (hf : RightInvOn f' f t) (ht : t₁ ⊆ t) : RightInvOn f' f t₁ :=
  LeftInvOn.mono hf ht

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