cancel_right — Mathlib

English

Equivalence between EqOn after composition and EqOn on original codomain given SurjOn and MapsTo.

Русский

Эквивалентность между равенством после композиции и равенством на исходном кодомном множестве при условии SurjOn и MapsTo.

LaTeX

$$$ \langle \mathrm{EqOn}(\,g_1\circ f)(\,g_2\circ f) \; s \rangle \leftrightarrow \mathrm{EqOn} g_1 g_2 t $$$

Lean4

theorem cancel_right (hf : s.SurjOn f t) (hf' : s.MapsTo f t) : s.EqOn (g₁ ∘ f) (g₂ ∘ f) ↔ t.EqOn g₁ g₂ :=
  ⟨fun h => h.cancel_right hf, fun h => h.comp_right hf'⟩

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