cancel_left — Mathlib

English

Left cancellation: if g is surjective, then g.trans f1 = g.trans f2 implies f1 = f2; and conversely, equality implies equality.

Русский

Левое сокращение: если g сюръективно, то g.trans f1 = g.trans f2 эквивалентно f1 = f2.

LaTeX

$$$\forall g: α \simeq^*o β,\; \forall f_1,f_2: β \simeq^*o γ,\; Surjective g \Rightarrow (g.trans f_1 = g.trans f_2) \iff (f_1 = f_2).$$$

Lean4

@[to_additive (attr := simp)]
theorem cancel_left {g : α ≃*o β} {f₁ f₂ : β ≃*o γ} (hg : Function.Surjective g) : g.trans f₁ = g.trans f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext <| hg.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

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