cancel_left — Mathlib

English

Let g be an injective FrameHom β γ. Then for all f1, f2: FrameHom α β, left-cancellation holds: g ∘ f1 = g ∘ f2 if and only if f1 = f2.

Русский

Пусть g — инъективный гомоморфизм рамки β→γ. Тогда для любых f1, f2: FrameHom α β выполняется тождество слева: g ∘ f1 = g ∘ f2 тогда и только тогда, когда f1 = f2.

LaTeX

$$$ g \\circ f_1 = g \\circ f_2 \\iff f_1 = f_2 \\quad (\\text{при условии, что } g \\text{ инъективен}) $$$

Lean4

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

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