English
Let g be an injective lattice homomorphism. Then precomposition with g is injective on the set of lattice homomorphisms: for all f1,f2, g∘f1 = g∘f2 iff f1 = f2.
Русский
Пусть g — инъективный гомоморфизм решётки. Тогда предварительная композиция с g инъективна: для любых f1,f2 выполняется g ∘ f1 = g ∘ f2 тогда и только тогда, когда f1 = f2.
LaTeX
$$$\forall g: LatticeHom(\beta,\gamma), \forall f_1,f_2: LatticeHom(\alpha,\beta), \text{Injective}(g) \Rightarrow (g \circ f_1 = g \circ f_2 \Leftrightarrow f_1 = f_2).$$$
Lean4
@[simp]
theorem cancel_left {g : LatticeHom β γ} {f₁ f₂ : LatticeHom α β} (hg : Injective g) :
g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
⟨fun h => LatticeHom.ext fun a => hg <| by rw [← LatticeHom.comp_apply, h, LatticeHom.comp_apply], congr_arg _⟩
