cancel_left — Mathlib

English

If g: InfTopHom β γ is injective, then g ∘ f1 = g ∘ f2 iff f1 = f2 for f1,f2: InfTopHom α β.

Русский

Пусть g: InfTopHom(β, γ) инъективен; тогда g ∘ f1 = g ∘ f2 эквивалентно f1 = f2 для f1,f2: InfTopHom(α, β).

LaTeX

$$$\\forall f_1,f_2:\\mathrm{InfTopHom}(\\alpha,\\beta),\\ (\\mathrm{Injective}(g)) \\Rightarrow (g\\circ f_1 = g\\circ f_2 \\iff f_1=f_2)$$$

Lean4

@[simp]
theorem cancel_left {g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => InfTopHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

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