comp_left — Mathlib

English

If h states that f1 and f2 agree on a set s, then composing both with g on the left preserves this agreement on s: g ∘ f1 and g ∘ f2 are equal on s.

Русский

Если f1 и f2 согласуются на множестве s, то после композиции слева с g их равенство сохраняется: g ∘ f1 и g ∘ f2 совпадают на s.

LaTeX

$$$ (EqOn\\ f_1\\ f_2\\ s) \\to EqOn\\ (g \\circ f_1)\\ (g \\circ f_2)\\ s $$$

Lean4

theorem comp_left (h : s.EqOn f₁ f₂) : s.EqOn (g ∘ f₁) (g ∘ f₂) := fun _ ha => congr_arg _ <| h ha

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