of_comp_iff — Mathlib

English

If g is bijective, then f ∘ g is bijective iff f is bijective.

Русский

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

LaTeX

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

Lean4

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

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