comp_ne_one_iff — Mathlib

English

Let f: α → β and a injective g: β → γ with g(1) = 1. Then g ∘ f ≠ 1 iff f ≠ 1.

Русский

Пусть f: α → β и инъективная g: β → γ с g(1) = 1. Тогда g ∘ f ≠ 1 эквивалентно f ≠ 1.

LaTeX

$$$ g \circ f \neq 1 \iff f \neq 1 $$$

Lean4

@[to_additive]
theorem comp_ne_one_iff [One β] [One γ] (f : α → β) {g : β → γ} (hg : Injective g) (hg0 : g 1 = 1) :
    g ∘ f ≠ 1 ↔ f ≠ 1 :=
  (comp_eq_one_iff f hg hg0).ne

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