cancel_right — Mathlib

English

If g is surjective, then f1 ∘ g = f2 ∘ g implies f1 = f2, and conversely (under surjectivity).

Русский

Если g сюръективен, то f1 ∘ g = f2 ∘ g эквивалентно f1 = f2; наоборот, эквивалентность следует из равенства композиций.

LaTeX

$$$\text{Surjective } g \Rightarrow (f_1 \circ g = f_2 \circ g \;\iff\; f_1 = f_2)$$$

Lean4

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

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