cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 implies f1 = f2; i.e., left-cancellation for pre-composition.

Русский

Если g инъективно, то g ∘ f1 = g ∘ f2 следует f1 = f2; левая отмена по композиции.

LaTeX

$$$\text{Injective } g \Rightarrow (g \circ f_1 = g \circ f_2 \;\text{ implies }\; f_1 = f_2)$$$

Lean4

@[simp]
theorem cancel_left {g : BoundedOrderHom β γ} {f₁ f₂ : BoundedOrderHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => BoundedOrderHom.ext fun a => hg <| by rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply],
    congr_arg _⟩

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