cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 if and only if f1 = f2.

Русский

Если g инъективно, то g ∘ f1 = g ∘ f2 тогда и только тогда, когда f1 = f2.

LaTeX

$$$\\\\forall g : \\\\operatorname{LocallyBoundedMap} \\\\beta \\\\gamma,\\\\forall f_1,f_2 : \\\\operatorname{LocallyBoundedMap} \\\\alpha \\\\beta, \\\\text{hg} : \\\\operatorname{Injective} (\\\\operatorname{coe} g), (g \\\\circ f_1) = (g \\\\circ f_2) \\\\iff f_1 = f_2.$$$

Lean4

@[simp]
theorem cancel_left {g : LocallyBoundedMap β γ} {f₁ f₂ : LocallyBoundedMap α β} (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 _⟩

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