cancel_left — Mathlib

English

The equivalence above is true as a standalone statement with the same hypotheses.

Русский

Эквивалентность выше истинна как самостоятельное утверждение при тех же предпосылках.

LaTeX

$$$ \\langle hg, hf_1, hf_2 \\rangle \\Rightarrow (s.EqOn (g \\circ f_1) (g \\circ f_2) \\iff s.EqOn f_1 f_2)$$$

Lean4

theorem cancel_left (hg : t.InjOn g) (hf₁ : s.MapsTo f₁ t) (hf₂ : s.MapsTo f₂ t) :
    s.EqOn (g ∘ f₁) (g ∘ f₂) ↔ s.EqOn f₁ f₂ :=
  ⟨fun h => h.cancel_left hg hf₁ hf₂, EqOn.comp_left⟩

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