cancel_right — Mathlib

English

If f: CompleteLatticeHom α β is surjective, then g1 ∘ f = g2 ∘ f iff g1 = g2.

Русский

Если f: CompleteLatticeHom α β сюръективен, то g1∘f = g2∘f тогда и только тогда, когда g1 = g2.

LaTeX

$$$\\text{Surjective } f\\;\\Rightarrow\\; g_1\\circ f = g_2\\circ f \\iff g_1 = g_2$$$

Lean4

@[simp]
theorem cancel_right {g₁ g₂ : CompleteLatticeHom β γ} {f : CompleteLatticeHom α β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, congr_arg (fun a ↦ comp a f)⟩

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