comp_bijective

Mathlib.Data.FunLike.Equiv

URI: https://scilib.ai/kg/mathlib#EquivLike.comp_bijective

English

Bijectivity of a composition e ∘ f is equivalent to the bijectivity of f.

Русский

Биективность композиции e ∘ f эквивалентна биективности f.

LaTeX

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

Lean4

@[simp]
theorem comp_bijective (f : α → β) (e : F) : Function.Bijective (e ∘ f) ↔ Function.Bijective f :=
  (EquivLike.bijective e).of_comp_iff' f

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru