bijective_comp — Mathlib

English

Let e be bijective in the EquivLike setting; then f ∘ e is bijective if and only if f is bijective.

Русский

Пусть e биективно отображает множества в контексте EquivLike; тогда f ∘ e биективно тогда и только тогда, когда биективен f.

LaTeX

$$$\text{Bijective}(e) \rightarrow \big(\text{Bijective}(f \circ e) \iff \text{Bijective}(f)\big)$$$

Lean4

@[simp]
theorem bijective_comp (e : E) (f : β → γ) : Function.Bijective (f ∘ e) ↔ Function.Bijective f :=
  (EquivLike.bijective e).of_comp_iff f

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