cancel_right — Mathlib

English

If f is surjective, then g1 ∘ f = g2 ∘ f implies g1 = g2; i.e., right-cancellation for post-composition.

Русский

Если f сюръективно, то g1 ∘ f = g2 ∘ f следует g1 = g2; правая отмена по композиции.

LaTeX

$$$\text{Surjective } f \Rightarrow (g_1 \circ f = g_2 \circ f \;\text{ implies }\; g_1 = g_2)$$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : BoundedOrderHom β γ} {f : BoundedOrderHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => BoundedOrderHom.ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun g => comp g f)⟩

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