cancel_right — Mathlib

English

Right cancellation: if f is injective, then g1.trans f = g2.trans f implies g1 = g2; and conversely, equality implies equality.

Русский

Правое исключение: если f инъективно, то g1.trans f = g2.trans f эквивалентно g1 = g2; и наоборот.

LaTeX

$$$\forall g_1,g_2: α \simeq^*o β,\; \forall f: β \simeq^*o γ,\; hf: Injective f \; \Rightarrow\; (g_1.trans f = g_2.trans f) \iff (g_1 = g_2).$$$

Lean4

@[to_additive (attr := simp)]
theorem cancel_right {g₁ g₂ : α ≃*o β} {f : β ≃*o γ} (hf : Function.Injective f) : g₁.trans f = g₂.trans f ↔ g₁ = g₂ :=
  ⟨fun h => ext fun a => hf <| by rw [← trans_apply, h, trans_apply], by rintro rfl; rfl⟩

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