of_comp_iff' — Mathlib

English

If f is bijective, then f ∘ g is bijective if and only if g is bijective.

Русский

Если f биективна, то f ∘ g биективна тогда и только тогда, когда g биективна.

LaTeX

$$$\operatorname{Bijective}(f) \Rightarrow \big( \operatorname{Bijective}(f \circ g) \iff \operatorname{Bijective}(g) \big).$$$

Lean4

theorem of_comp_iff' {f : α → β} (hf : Bijective f) (g : γ → α) : Function.Bijective (f ∘ g) ↔ Function.Bijective g :=
  and_congr (Injective.of_comp_iff hf.injective _) (Surjective.of_comp_iff' hf _)

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