comp_eq_one_iff — Mathlib

English

Let f: α → β and g: β → γ be such that g is injective and g(1) = 1. Then g ∘ f = 1 if and only if f = 1.

Русский

Пусть f: α → β и g: β → γ, причём g инъективна и g(1) = 1. Тогда g ∘ f = 1 тогда и только тогда, когда f = 1.

LaTeX

$$$ g \circ f = 1 \iff f = 1 \quad \text{(with } hg: Injective\ g,\; hg0: g 1 = 1\text{)}}$$$

Lean4

@[to_additive]
theorem comp_eq_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :
    g ∘ f = 1 ↔ f = 1 := by simpa [hg0, const_one] using comp_eq_const_iff 1 f hg

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