cancel_left — Mathlib

English

If g is injective, then g ∘ f1 = g ∘ f2 iff f₁ = f₂ for complete lattice homomorphisms g, f1, f2.

Русский

Если g инъективен, то g∘f1 = g∘f2 тогда и только тогда, когда f₁ = f₂ для гомоморфизмов полной решётки.

LaTeX

$$$\\text{Injective } g\\;\\Rightarrow\\; g\\circ f_1 = g\\circ f_2 \\iff f_1 = f_2$$$

Lean4

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

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